Correspondence between Types and Topological spaces
Homotopy Type Theory (LMFI)
Examples of inductive types:
HIT: Inductive types where equality is also taken into account.
[μC. (C ⟶ C)]
We want a notion of category where type is a category, so that there’s a notion of homotopy thanks to model structures.
Category in 2-level type theory