Zigzag normalisation for associative n-categories

DOI10.1145/3531130.3533352arXiv2205.08952MaRDI QIDQ6399491FDOQ6399491

Authors: Lukas Heidemann, David Reutter, Jamie Vicary 

Publication date: 18 May 2022

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.

This page was built for publication: Zigzag normalisation for associative $n$-categories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6399491)