We construct a left semi-model structure on the category of intensional type theories (precisely, on CxlCat_{Id,1,Σ(,Πext)}). This presents an infinity-category of such type theories; we show moreover that there is an infinity-functor Cl_∞ from there to the infinity-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.