Zigzag normalisation for associative $n$-categories

TL;DR

This paper introduces a recursive zigzag-based normalisation method for associative n-categories, simplifying the theory and enabling efficient proof assistant implementation.

Contribution

It presents a novel categorical zigzag approach to term normalisation in associative n-categories, providing a recursive algorithm with correctness proof.

Findings

The normalisation algorithm is correct and recursive.

The approach simplifies the theory of associative n-categories.

The method is implemented in the proof assistant homotopy.io.

Abstract

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.