Homotopy Type Theory
Category theory

Here we collect articles about doing category theory in HoTT. This is based off of the HoTT Book.

Definitions

Groupoids

Homotopy precategories

Morphisms

Categories

Functors

Limits and colimits

Dagger morphisms

Dagger categories

Order theory

2-posets

dagger 2-posets

Dagger morphisms in dagger 2-posets

Concrete categories

Theorems

References