formal category theory

Last updated Sep 8, 2023

• Section 0: The setup
  • double category
  • proarrow equipment
  • Companions and conjoints
  • Double category CAT
• Section 1: 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)