Formalizing parity complexes

TL;DR

This paper formalizes the initial parts of the theory of parity complexes in Coq, verifying complex recursive algorithms and definitions that underpin the construction of free ω-categories from combinatorial structures.

Contribution

It provides a formal Coq implementation of parity complexes up to the excision of extremals, ensuring correctness and clarifying which parts require complex proofs.

Findings

Formal verification of all cases in the theory

Identification of parts requiring complex proofs

Insights into future research directions

Abstract

We formalise, in Coq, the opening sections of Parity Complexes [Street1991] up to and including the all important excision of extremals algorithm. Parity complexes describe the essential combinatorial structure exhibited by simplexes, cubes and globes, that enable the construction of free $\omega$-categories on such objects. The excision of extremals is a recursive algorithm that presents every cell in such a category as a (unique) composite of atomic cells. This is the sense in which the $\omega$-category is (freely) generated from its atoms. Due to the complicated multi-dimensional nature of this work, the detail of definitions and proofs can be hard to follow and verify. Indeed, some corrections were required some years following the original publication~\cite{Street1994}. Our formalisation verifies that all cases of each result operate as stated. In particular, we indicate which portions of the theory can be proved directly from definitions, and which require more subtle and complex arguments. By identifying results that require the most complicated proofs, we are able to investigate where this theory might benefit from further study and which results need to be considered most carefully in future work.