[[!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]] ### Limits and colimits ### * [[product]] * [[coproduct]] * [[equaliser]] * [[directed colimit]] ### 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]] ### Order theory ### * [[preorder]] * [[directed type]] * [[net]] * [[poset]] * [[join-semilattice]] * [[meet-semilattice]] * [[omega-complete poset]] * [[directed-complete poset]] * [[partial function classifier]] * [[Sierpinski space]] * [[continuous poset]] * [[lattice]] * [[distributive lattice]] * [[sigma-complete lattice]] * [[sigma-frame]] * [[suplattice]] * [[frame]] * [[Heyting algebra]] * [[Boolean algebra]] * [[monotonic function]] * [[monotonic function preorder]] * [[sigma-continuous function]] * [[opposite preorder]] * [[antitonic function]] * [[posite]] * [[lower type]] * [[upper type]] * [[ideal]] * [[filter]] * [[enriched poset]] * [[order]] * [[strict order]] * [[dense strict order]] * [[quasiorder]] * [[strict lower type]] * [[strict upper type]] * [[Dedekind cut]] * [[Dedekind complete dense strict order]] ### 2-posets ### * [[2-preorder]] * [[2-poset]] * [[locally Heyting-algebraic 2-poset]] ### dagger 2-posets ### * [[dagger 2-preorder]] * [[dagger 2-poset]] * [[semiadditive dagger 2-poset]] * [[unital dagger 2-poset]] * [[tabular dagger 2-poset]] * [[division dagger 2-poset]] * [[power dagger 2-poset]] * [[cartesian dagger 2-poset]] * [[conjunctive dagger 2-poset]] * [[coherent dagger 2-poset]] * [[Heyting dagger 2-poset]] * [[Boolean dagger 2-poset]] * [[elementarily topical dagger 2-poset]] * [[Boolean topical dagger 2-poset]] * [[W-topical dagger 2-poset]] * [[well-pointed dagger 2-poset]] * [[choice dagger 2-poset]] * [[category of maps]] ### Dagger morphisms in dagger 2-posets ### * [[onto dagger morphism in a dagger 2-poset]] * [[functional dagger morphism in a dagger 2-poset]] * [[entire dagger morphism in a dagger 2-poset]] * [[one-to-one dagger morphism in a dagger 2-poset]] * [[map in a dagger 2-poset]] * [[injection in a dagger 2-poset]] * [[surjection in a dagger 2-poset]] ### Concrete categories ### * [[concrete precategory]] * [[concrete category]] * [[concrete dagger 2-poset]] * [[HilbR]] * [[Rel]] * [[ETCR]] * [[Categorical SEAR]] * [[SEAR]] ### Higher categories ### * [[(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]] category: category theory,navigation