论文标题
严格的Unital $ \ infty $ - 类别的类型理论
A Type Theory for Strictly Unital $\infty$-Categories
论文作者
论文摘要
我们使用类型理论技术来提出具有严格单位的$ \ infty $类别的代数理论。从完全弱$ \ infty $ - 类别的已知类型理论表现开始，其中表示有效的操作，我们以非平凡的定义平等扩展了理论。这迫使某些操作严格在任何模型中重合，从而产生严格的单位行为。 我们对该理论的元理论特性进行了详细的研究。我们提供了一个减少关系，从而产生定义平等，并证明它是汇合和终止的，从而在严格的非军事环境中产生了平等的第一个决策程序。此外，我们表明我们的定义平等关系在光盘上下文中标识了所有术语，从而与先前提出的严格Unital $ \ infty $ -scategory的定义进行了比较。我们还证明了保守性结果，这表明严格的Unital理论的每一次操作确实源于完全弱理论中的有效操作。由此，我们推断出严格的单位性是$ \ infty $类别的属性，而不是其他结构。
We use type-theoretic techniques to present an algebraic theory of $\infty$-categories with strict units. Starting with a known type-theoretic presentation of fully weak $\infty$-categories, in which terms denote valid operations, we extend the theory with a non-trivial definitional equality. This forces some operations to coincide strictly in any model, yielding the strict unit behaviour. We make a detailed investigation of the meta-theoretic properties of this theory. We give a reduction relation that generates definitional equality, and prove that it is confluent and terminating, thus yielding the first decision procedure for equality in a strictly-unital setting. Moreover, we show that our definitional equality relation identifies all terms in a disc context, providing a point comparison with a previously proposed definition of strictly unital $\infty$-category. We also prove a conservativity result, showing that every operation of the strictly unital theory indeed arises from a valid operation in the fully weak theory. From this, we infer that strict unitality is a property of an $\infty$-category rather than additional structure.
