[[!redirects Category theory in HoTT]] Here we collect articles about doing category theory in HoTT. This is based off of the [[HoTT Book]]. ## Definitions ## * [[precategory]] * [[isomorphism]] * [[category]] * [[functor]] * [[natural transformation]] * [[functor precategory]] * [[left adjoint]] * [[equivalence of precategories]] * [[faithful functor]] * [[full functor]] * [[split essentially surjective]] * [[essentially surjective]] * [[weak equivalence of precategories]] * [[isomorphism of precategories]] * [[opposite precategory]] * [[product precategory]] * [[hom functor]] ## Theorems ## * [[Rezk completion]] * [[Yoneda lemma]] ## References ## * [[HoTT Book]] * [Univalent categories and the Rezk completion](https://arxiv.org/abs/1303.0584) by Benedikt Ahrens, Chris Kapulkin, Michael Shulman. category: category theory,navigation