We present the first definition of strictly associative and unital $\infty$-category. Our proposal takes the form of a type theory whose terms describe the operations of such structures, and whose definitional equality relation enforces desired strictness conditions. The key technical device is a new computation rule in the definitional equality of the theory, which we call insertion, defined in terms of a universal property. On terms for which it is defined, this operation "inserts" one of the arguments of a substituted coherence into the coherence itself, appropriately modifying the pasting diagram and result type, and simplifying the syntax in the process. We generate an equational theory from this reduction relation and we study its properties in detail, showing that it yields a decision procedure for equality. Expressed as a type theory, our model is well-adapted for generating and verifying efficient proofs of higher categorical statements. We illustrate this via an OCaml implementation, and give a number of examples, including a short encoding of the syllepsis, a 5-dimensional homotopy that plays an important role in the homotopy groups of spheres.

翻译：我们提出了首个严格结合且幺元的∞-范畴定义。我们的方案以类型理论的形式呈现，其项描述了此类结构的运算，其定义相等关系则强制执行所需的严格性条件。关键技术手段是理论定义相等中的一条新计算规则，我们称之为插入操作，该操作通过泛性质定义。对于可应用此项操作的项，该操作将替换的相干性中的一个参数“插入”到相干性自身中，相应修改粘贴图与结果类型，并在此过程中简化语法。我们从该约化关系生成等式理论，并详细研究其性质，证明其可产生判定相等性的过程。以类型理论表述的模型非常适用于生成并验证高阶范畴陈述的高效证明。我们通过OCaml实现加以说明，并提供若干示例，包括对syllepsis（一个在球面同伦群中起重要作用的五维同伦）的简短编码。