Zigzag normalisation for associative -categories
arXiv:2205.08952 · doi:10.1145/3531130.3533352
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. This normalisation algorithm forms a core component of the proof assistant homotopy.io, and we illustrate our scheme with worked examples.
References in corpus (9)
- Higher-dimensional Algebra and Topological Quantum Field Theory
- A survey of graphical languages for monoidal categories
- The Classification of Two-Dimensional Extended Topological Field Theories
- Homotopy theoretic models of identity types
- Notes on Grothendieck topologies, fibered categories and descent theory
- Higher-dimensional normalisation strategies for acyclicity
- Biunitary constructions in quantum information
- Towards 3-Dimensional Rewriting Theory
- Holographic Software for Quantum Networks