论文标题
$ \ infty $ -type理论
$\infty$-type theories
论文作者
论文摘要
我们将$ \ infty $ -type理论作为$ \ infty $ - 分类概括，对第二名作者引入的类型理论的分类定义。我们建立了类似的结果，包括$ \ infty $ -Type理论的初始模型，$ \ infty $ type理论的内部语言的构建以及$ \ infty $ type理论的理论模型通信。一些结构化的$（\ infty，1）$ - 类别自然被视为某些$ \ infty $ type理论的模型。因此，由于每个（1类）类型理论尤其是$ \ infty $ -type理论，因此$ \ infty $ type理论为类型理论与$（\ infty，1）$分类结构之间的连接提供了一个统一的框架。作为一个应用程序，我们证明了Kapulkin和Lumsdaine的猜想，即具有强度身份类型的因类型理论提供了$（\ Infty，1）$ - 具有有限限制的类别的内部语言。
We introduce $\infty$-type theories as an $\infty$-categorical generalization of the categorical definition of type theories introduced by the second named author. We establish analogous results to the previous work including the construction of initial models of $\infty$-type theories, the construction of internal languages of models of $\infty$-type theories, and the theory-model correspondence for $\infty$-type theories. Some structured $(\infty,1)$-categories are naturally regarded as models of some $\infty$-type theories. Thus, since every (1-categorical) type theory is in particular an $\infty$-type theory, $\infty$-type theories provide a unified framework for connections between type theories and $(\infty,1)$-categorical structures. As an application we prove Kapulkin and Lumsdaine's conjecture that the dependent type theory with intensional identity types gives internal languages for $(\infty,1)$-categories with finite limits.
