The homotopy theory of type theories (Q1785779)

The internal language conjecture is the idea that HoTT should be the internal language of \(\infty\)-categories. The first main contribution of the paper is to provide a framework for formulating such a claim precisely. The authors assemble intensional type theories into a higher category, and give a functor \(\mathrm{Cl}_\infty\) from this to a higher category of suitable structured quasicategories. The internal language conjecture can then be stated as: \(\mathrm{Cl}_\infty\) is an equivalence of higher categories. The second main contribution of the paper is a left semi-model structure on the category of intensional type theories.