KittyCats

A Lean formalization of undergraduate category theory built from first principles with no Mathlib.

• Category - categories, composition, identity, and the opposite category
• Functor - functors, identity functor, functor composition
• NatTrans - natural transformations, vertical composition, natural isomorphisms
• Morphism - isomorphisms, monomorphisms, epimorphisms, split monos/epis, groupoids
• Product - the product of two categories
• Limits - terminal and initial objects, categorical products, coproducts
• Cartesian - cartesian and cocartesian categories, diagonal, product maps
• Monoidal - monoidal, braided, and symmetric monoidal categories
• Closed - exponential objects, cartesian closed categories
• Dual - the duality principle: terminal/initial, product/coproduct, mono/epi via Op
• Equiv - equivalence of categories, the Op involution
• Instances - the category of types as a cartesian closed category
• Adjunction - adjunctions via unit/counit with triangle identities
• Monad - monads, Kleisli categories, monads as monoids in the category of endofunctors
• Thm - naturality of pairing, diagonal absorption, and the curry/eval adjunction
• Yoneda - presheaves, the Yoneda lemma, fully faithful embedding

Refs

• Steve Awodey, Category Theory (2nd edition, Oxford Logic Guides, 2010).
• Saunders Mac Lane, Categories for the Working Mathematician (2nd edition, Springer GTM, 1998).

License

MIT