一句话：提出结合 n-范畴项规范化的 zigzag 构造算法，证明其正确性，并用于证明助手 homotopy.io。
Associative n-范畴为高阶范畴论提供了一种严格结合且含单位的表述，有望作为证明助手的基础，从而形式化复杂的高维代数现象。然而，该理论依赖隐式的项规范化过程来判定正确的复合，此前没有可递归计算的方法。本文基于范畴的 zigzag 构造提出新的项规范化方法，显著简化理论，并给出递归规范化算法，证明其正确性。作者利用范畴提升性质高效证明结果。该算法已成为证明助手 homotopy.io 的核心组件，文中还给出多个实例说明其工作方式。
The theory of associative n-categories has recently been proposed as a strictly associative and unital approach to higher category theory. As a foundation for a proof assistant, this is potentially attractive, since it has the potential to allow simple formal proofs of complex high-dimensional algebraic phenomena. However, the theory relies on an implicit term normalisation procedure to recognize correct composites, with no recursive method available for computing it. Here we describe a new approach to term normalisation in associative n-categories, based on the categorical zigzag construction. This radically simplifies the theory, and yields a recursive algorithm for normalisation, which we prove is correct. Our use of categorical lifting properties allows us to give efficient proofs of our results. Our normalisation algorithm forms a core component of the proof assistant homotopy.io, and we illustrate our scheme with worked examples.