类型理论的同伦理论

我们在内涵类型理论范畴（确切地说，在 $\mathrm{CxlCat_{Id,1,\Sigma(,\Pi_{ext})}}$ 上）构造了一个左半模型结构。这给出了此类类型理论的一个 $\infty$-范畴；我们进一步证明，存在一个从该范畴到具有适当结构的拟范畴的 $\infty$-范畴的 $\infty$-函子 $\mathrm{Cl}_\infty$。这使得“内涵类型理论为高阶范畴提供内部语言”这一猜想得以精确表述，并为这些猜想的进一步研究提供了一个框架与工具箱。