The homotopy theory of type theories

Abstract

We construct a left semi-model structure on the category of intensional type theories (precisely, on $\mathrm{CxlCa}{\mathrm{t}}_{\mathrm{Id},1,\mathrm{\Sigma }(,{\mathrm{\Pi }}_{\mathrm{ext}})}$). This presents an $\infty$-category of such type theories; we show moreover that there is an $\infty$-functor ${\mathrm{Cl}}_{\infty }$ from there to the $\infty$-category of suitably structured quasi-categories. This allows a precise formulation of the conjectures that intensional type theory gives internal languages for higher categories, and provides a framework and toolbox for further progress on these conjectures.

v2: revised for release of companion paper arXiv:1808.01816; some theorem numbering changes