[[!redirects category theory]] [[!redirects Category theory in HoTT]] Here we collect articles about doing category theory in HoTT. ## Definitions ## ### Groupoids ### * [[pregroupoid]] * [[setoid]] * [[groupoid]] * [[set]] ### Homotopy precategories ### * [[quiver]] * [[directed graph]] * [[H-magmoid]] * [[H-spaceoid]] * [[homotopy precategory]] * [[concrete homotopy precategory]] * [[family of objects in a concrete homotopy precategory]] * [[SEPS]] ### Morphisms ### * [[isomorphism in a precategory]] * [[epimorphism in a precategory]] * [[monomorphism in a precategory]] ### Categories ### * [[precategory]] * [[category]] * [[equivalence of precategories]] * [[opposite precategory]] ### 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]] ### 2-posets ### * [[2-preorder]] * [[2-poset]] ### Concrete categories ### * [[concrete precategory]] * [[concrete category]] * [[SEAR]] category: category theory,navigation