依赖类型理论的内部∞-范畴模型：迈向 2LTT 消化 HoTT

使用依赖类型理论来形式化依赖类型理论的语法是一个十分活跃的研究课题，被称为“类型理论消化自身”或“类型理论中的类型理论”。大多数方法至少松散地基于 Dybjer 的带族范畴（CwF），并带有一个语境类型 CON、一个在其上索引以建模类型的类型族 TY，等等。这在唯一同一性证明原理（UIP）成立的类型理论版本中运作良好。然而，在同伦类型理论（HoTT）中，类型理论是否“消化自身”并可作为其自身的解释器，是一个长期且频繁讨论的开放问题。其根本困难似乎在于，在缺乏 UIP 的情况下，范畴并不适合刻画类型理论。在本文中，我们发展了带族∞-范畴（∞-CwF）的概念。所使用的高阶范畴方法依赖于先前提出的半 Segal 类型，并带有一种新的同一性替换构造，允许酉变与非酉变两种变体。类型论宇宙以及内部化语法都是模型，尽管后者为初始模型仍是一个猜想。为规避构造半单纯类型的已知未解问题，该定义在两能级类型理论（2LTT）中给出。除引入∞-CwF 外，本文还解释了无 UIP 的类型理论中 1-范畴的缺陷，以及内部高阶范畴的困难与方法。