Zigzag normalisation for associative n-categories
Accepted version
Peer-reviewed
Repository URI
Repository DOI
Change log
Authors
Abstract
The theory of associative 𝑛-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 𝑛-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 a proof assistant, and we illustrate our scheme with worked examples.
Description
Keywords
Journal Title
Conference Name
Journal ISSN
Volume Title
Publisher
Publisher DOI
Rights
Sponsorship
Royal Society (RGF\R1\180097)
Royal Society (RGF\EA\180288)
Royal Society (UF160476)
Royal Society (RGF\EA\201079)