[[!redirects category theory]] [[!redirects Category theory in HoTT]] 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]] ## Theorems ## * [[Rezk completion]] * [[Yoneda lemma]] ## References ## * [[HoTT Book]] * [[Univalent categories and the Rezk completion]] category: category theory,navigation