Repository logo
 

Zigzag normalisation for associative n-categories

Accepted version
Peer-reviewed

Loading...
Thumbnail Image

Type

Conference Object

Change log

Authors

Vicary, Jamie 
Reutter, David 
Rice, Alex 
Finster, Eric 

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

Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science

Conference Name

LICS 2022

Journal ISSN

Volume Title

Publisher

Association for Computing Machinery
Sponsorship
EPSRC (EP/S018646/2)
Royal Society (RGF\R1\180097)
Royal Society (RGF\EA\180288)
Royal Society (UF160476)
Royal Society (RGF\EA\201079)