Homotopy Type Theory category theory > history (Rev #68)

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