Being a lean deveopment for various bits of category theory I happen to be interested in.
Some particular goals include developing:
- enough of the theory of cartesian closed categories to cover semantics of STLC
- the fibrational models of system F
- the 2-yoneda lemma for bicategories and using it to prove coherence of monoidal categories
- the theory of lattices / pointless topology
- the theory of sites, subobject classifiers for presheaf cats, the canonical topology, the double negation topology and elementary forcing
- Grothendieck's galois theory
lake build CategoryTheory