formal category theory

Last updated May 3, 2024

• Setup.

  • double category
  • proarrow equipment
  • Companions and conjoints
  • Double category CAT

• Proarrow equipments for formal category theory

  • monoids and promonoids
  • Promonoids from monoids
  • Monoids and comonoids induce promonoids in a proarrow equipment
  • Monad
  • promonad
  • Adjunctions in a proarrow equipment
  • distributive law (+)
  • Distributive laws of monoids and comonoids induce distributive laws of promonoids
  • Proalgebra of a promonad
  • Kleisli object

• Section 2: Monoidal proarrow equipments for monoidal category theory

  • Strong promonad
  • Prostrong promonad
  • Monoidal double category of categories
  • pseudomonoid
  • promonoidal category
  • Right adjoint to oplax is lax
  • Interaction laws

• Section 3: Extra syntax

  • Weighted colimits in box notation
  • What is special about Set, in the double category Cat
  • Reversors in profunctors
  • Diagrammatic formal dualities

References

• Category Theory Using String Diagrams (Marsden, 2014)
• String Diagrams for Double Categories and Equipments (Myers, 2016)
• A Formal Logic for Formal Category Theory (New, Licata, 2022)