A Type Theory for Strictly Unital 8-Categories
A Type Theory for Strictly Unital 8-Categories
复制标题
严格统一 8 类的类型理论
DOI：
10.1145/3531130.3533363
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Finster E
中科院分区：
文献类型：
--
作者：
Finster E
我们利用类型论的技巧给出了严格单位的∞-范畴的代数理论。从一个已知的完全弱∞-范畴的类型论表示开始，其中项表示有效运算，我们用一个非平凡的定义等式扩展了该理论。这迫使一些操作严格符合任何模型，产生严格的单位行为。我们做了详细的调查，这个理论的元理论的性质。我们给出了一个约化关系，产生定义的平等，并证明了它是合流和终止，从而产生的第一个决定程序的平等在严格的单位设置。此外，我们表明，我们的定义的等式关系确定所有的条款，在一个磁盘的上下文中，提供了一个点比较与以前提出的定义严格酉∞-范畴。我们还证明了一个保守性结果，表明严格么正理论的每一个操作确实产生于完全弱理论中的有效操作。由此，我们推断严格么正性是一个∞-范畴的性质，而不是附加结构。
We use type-theoretic techniques to present an algebraic theory of ∞-categories with strict units. Starting with a known type-theoretic presentation of fully weak ∞-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 ∞-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 ∞-category rather than additional structure.