Homotopy Type Theory category theory > history (Rev #4, changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

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

Definitions

• precategory
• isomorphism?
• category
• functor
• natural transformation
• functor precategory
• left adjoint
• equivalence of categories?
• faithful functor
• full functor
• split essentially surjective
• essentially surjective
• weak equivalence
• isomorphism of precategories?
• opposite precategory
• product precategory

Theorems

• Rezk completion
• Yoneda lemma