The homotopy theory of type theories

We construct a left semi-model structure on the category of intensional type theories (precisely, on $\mathrm{C}\mathrm{x}\mathrm{l}\mathrm{C}\mathrm{a}{\mathrm{t}}_{\mathrm{I}\mathrm{d},1,\mathrm{\Sigma }(,{\mathrm{\Pi }}_{\mathrm{e}\mathrm{x}\mathrm{t}})}$). This presents an $\mathrm{\infty }$-category of such type theories; we show moreover that there is an $\mathrm{\infty }$-functor ${\mathrm{C}\mathrm{l}}_{\mathrm{\infty }}$ from there to the $\mathrm{\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.