Sets in homotopy type theory

Egbert Rijke, Bas Spitters

Homotopy Type Theory may be seen as an internal language for the $\infty$-category of weak $\infty$-groupoids which in particular models the univalence axiom. Voevodsky proposes th…