Homotopy Type Theory category theory > history (Rev #18)

Here we collect articles about doing category theory in HoTT. This is based off of the HoTT Book.

Definitions

Morphisms

• isomorphism in a precategory
• epimorphism in a precategory?
• monomorphism in a precategory?

Categories

• precategory
• category
• equivalence of precategories
• weak equivalence of precategories
• isomorphism of precategories?
• opposite precategory
• product precategory

Functors

• functor
• natural transformation
• functor precategory
• left adjoint
• faithful functor
• full functor
• split essentially surjective
• essentially surjective
• hom functor
• representable functor

Dagger morphisms

• unitary isomorphism in a dagger precategory
• dagger epimorphism in a dagger precategory
• dagger monomorphism in a dagger precategory

Dagger categories

• dagger precategory
• dagger category
• monoidal dagger category
• braided monoidal dagger category
• symmetric monoidal dagger category
• cartesian monoidal dagger category
• cocartesian monoidal dagger category
• semiadditive dagger category
• finitely complete dagger category?
• finitely cocomplete dagger category?
• compact closed dagger category

Higher categories

• 2-preorder
• 2-poset
• (2,1)-precategory?
• (2,1)-category?
• (2,2)-precategory?
• (2,2)-category?
• 3-preorder?
• 3-poset?

Theorems

• Rezk completion
• Yoneda lemma

References

• HoTT Book
• Univalent categories and the Rezk completion