一句话：用类型论刻画带严格单位的 ∞-范畴，给出定义相等性的归约判定过程，并证明严格单位性是性质而非结构。
本文为带严格单位的 ∞-范畴建立代数理论。作者从已有的完全弱 ∞-范畴的类型论表示出发，引入非平凡的定义相等性，使某些操作在任何模型中严格重合，从而得到严格单位行为。文章系统研究该理论的元理论性质：给出生成定义相等性的归约关系，证明其合流且终止，得到严格单位设定下第一个相等性判定过程；证明该定义相等性在 disc 语境中可识别所有项，并与此前严格单位 ∞-范畴的定义比较；还证明保守性，即严格单位理论的操作均来自完全弱理论中的有效操作。由此推出严格单位性是 ∞-范畴的性质而非额外结构。
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.