Homotopy Type Theory category theory > history (Rev #70, changes)

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

Categories

• precategory
• category

Dagger morphisms

• unitary isomorphism in a dagger precategory

Dagger categories

• dagger precategory
• dagger category

2-posets

• 2-preorder
• 2-poset

Concrete categories

• concrete precategory
• concrete category
• SEAR