内部$\infty$ -依赖类型论的分类模型：走向2LTT进食HoTT
Internal $\infty$-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT
摘要：
使用依赖类型论来形式化依赖类型论的句法是一个非常活跃的研究课题，并被称为“类型论吃自己”或“类型论中的类型论”。大多数方法至少是松散地基于Dybjer的带族的范畴（CwF），并带有上下文的类型CON，在其上索引的类型族TY建模类型，等等。这在类型论的版本中工作得很好，其中唯一身份证明（UIP）原则成立。然而，在同伦类型论（HoTT）中，类型论是否“吃自己”并能作为自己的解释者是一个长期存在且经常讨论的公开问题。基本的潜在困难似乎是，在没有UIP的情况下，范畴不适合捕捉类型论。在本文中，我们提出了$\infty$ -含族范畴（$\infty$ -CwF's）的概念.使用的方法，以更高的类别依赖于以前建议的半Segal类型，与一个新的建设的身份取代，允许单价和非单价的变化。类型论的宇宙以及内在化的语法都是模型，尽管后者是初始的仍然是一个猜想。为了避免已知的未解决的问题，构造半单纯型，定义在两级类型论（2LTT）。本文除了介绍$\infty$外，还说明了在没有UIP的类型论中1-范畴的缺点，以及内部高维范畴的困难和途径。
英文摘要：
Using dependent type theory to formalise the syntax of dependent type theory is a very active topic of study and goes under the name of "type theory eating itself" or "type theory in type theory." Most approaches are at least loosely based on Dybjer's categories with families (CwF's) and come with a type CON of contexts, a type family TY indexed over it modelling types, and so on. This works well in versions of type theory where the principle of unique identity proofs (UIP) holds. In homotopy type theory (HoTT) however, it is a long-standing and frequently discussed open problem whether the type theory "eats itself" and can serve as its own interpreter. The fundamental underlying difficulty seems to be that categories are not suitable to capture a type theory in the absence of UIP. In this paper, we develop a notion of $\infty$-categories with families ($\infty$-CwF's). The approach to higher categories used relies on the previously suggested semi-Segal types, with a new construction of identity substitutions that allow for both univalent and non-univalent variations. The type-theoretic universe as well as the internalised syntax are models, although it remains a conjecture that the latter is initial. To circumvent the known unsolved problem of constructing semisimplicial types, the definition is presented in two-level type theory (2LTT). Apart from introducing $\infty$-CwF's, the paper explains the shortcomings of 1-categories in type theory without UIP as well as the difficulties of and approaches to internal higher-dimensional categories.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
