We present the first definition of strictly associative and unital $\infty$-category. Our proposal takes the form of a generalized algebraic theory, with operations that give the composition and coherence laws, and equations encoding the strict associative and unital structure. The key technical idea of the paper is an equality generator called insertion, which can ``insert'' an argument context into the head context, simplifying the syntax of a term. The equational theory is defined by a 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.

翻译：本文首次给出了严格结合且具有幺元的$\infty$-范畴的定义。我们的方案采用广义代数理论的形式，其中运算定义了复合与协调法则，而方程编码了严格的结合与幺元结构。论文的关键技术思想是一种称为插入的等式生成器，它可以将"论元语境"插入到"头部语境"中，从而简化项的语法。等式理论通过归约关系定义，我们详细研究了其性质，证明它能为相等性提供判定过程。若将其表述为类型理论，我们的模型非常适用于生成和验证高阶范畴陈述的有效证明。我们通过OCaml实现进行说明，并给出若干示例，其中包括对5维同伦映射（其中在球面同伦群中起重要作用的syllepsis）的简短编码。