Homotopy Type Theory
Category theory
Here we collect articles about doing category theory in HoTT. This is based off of the HoTT Book.
Definitions
Groupoids
Homotopy precategories
Morphisms
Categories
Functors
Limits and colimits
- product?
- coproduct?
- equaliser?
- directed colimit?
Dagger morphisms
Dagger categories
Order theory
2-posets
dagger 2-posets
Dagger morphisms in dagger 2-posets
Concrete categories
Theorems
References