A formal verification of the theory of parity complexes


  • Mitchell Buckley Macquarie University




parity complex, omega category, category, pasting diagram, excision of extremals


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 composite of atomic cells, this is the sense in which the omega category is free. 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 [Street1994] were required some years following the original publication.

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.


Iain R. Aitchison. The geometry of oriented cubes. Macquarie University Research Report No: 86-0082, 1986.

Fahd Ali Al-Agl and Richard Steiner. Nerves of multiple categories. Proc. London Math. Soc. (3), 66(1):92-128, 1993.

Michael Johnson. Pasting diagrams in n-categories with applications to coherence theorems and categories of paths. PhD thesis, University of Sydney, 1988.

Michael Johnson. The combinatorics of n-categorical pasting. J. Pure Appl. Algebra, 62(3):211-225, 1989.

The Coq development team. The Coq proof assistant reference manual (v8.4), 2014.

Richard Steiner. The algebra of directed complexes. Appl. Categ. Structures, 1(3):247-284, 1993.

Richard Steiner. Omega-categories and chain complexes. Homology Homotopy Appl., 6(1):175-200, 2004.

Ross Street. The algebra of oriented simplexes. Journal of Pure and Applied Algebra, 49(3):283-335, 1987.

Ross Street. Parity complexes. Cahiers de Topologie et Géométrie Différentiel le Catégoriques, 32(4):315-343, 1991.

Ross Street. Parity complexes: Corrigenda. Cahiers de Topologie et Géométrie Différentiel le Catégoriques, 35(4):359-361, 1994.

Ross Street. Higher categories, strings, cubes and simplex equations. Appl. Categ. Structures, 3(1):29-77, 1995.

Dominic Verity. Complicial sets characterising the simplicial nerves of strict ω-categories. Mem. Amer. Math. Soc., 193(905):xvi+184, 2008.




How to Cite

Buckley, M. (2015). A formal verification of the theory of parity complexes. Journal of Formalized Reasoning, 8(1), 25–48. https://doi.org/10.6092/issn.1972-5787/5010