Homotopy Type Theory
Category theory (changes)

Showing changes from revision #12 to #13: Added | Removed | Changed

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

Definitions

Morphisms

• isomorphism?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

Theorems

• Rezk completion
• Yoneda lemma

References

• HoTT Book
• Univalent categories and the Rezk completion by Benedikt Ahrens, Chris Kapulkin, Michael Shulman.