论文标题
关联$ n $类别的曲折标准化
Zigzag normalisation for associative $n$-categories
论文作者
论文摘要
联想性$ n $类别的理论最近被提议是一种严格的关联和统一方法，以实现高等类别理论。作为证明助手的基础，这可能具有吸引力，因为它有可能允许简单的形式证明复杂的高维代数现象。但是，该理论依赖于隐式术语归一化过程来识别正确的复合材料，而没有可用于计算它的递归方法。 在这里，我们根据分类的曲折构造描述了一种新的方法，以相关性$ n $类别中的术语归一化方法。从根本上讲，这简化了理论，并得出了用于归一化的递归算法，我们证明这是正确的。我们使用分类提升属性使我们能够有效地证明我们的结果。该归一化算法构成了证明助手同型的核心组成部分，我们用有效的示例说明了我们的方案。
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. This normalisation algorithm forms a core component of the proof assistant homotopy.io, and we illustrate our scheme with worked examples.
