Single-set cubical categories and their formalisation with a proof assistant (extended version)

TL;DR

This work develops a $single-set$ axiomatisation of cubical $ω$-categories, incorporating connections and inverses, and justifies it by establishing precise equivalences with classical cubical theories. The approach relies on a per-direction family of structures with symmetry maps and a lattice of fixed points to model higher identities, together with truncation to finite dimensions. A central contribution is the demonstration that the single-set framework is equivalent to the classical cubical, connection, and inverse theories via the functors ${(-)}^{c}$ and ${(-)}^{s}$ and their natural isomorphisms, extended to $(ω,p)$-settings. The Isabelle/HOL formalisation is instrumental in taming the axioms, automating proofs, and validating the equivalences, illustrating the practical potential of proof assistants for higher-dimensional rewriting and related areas. The results open avenues for formalised higher category theory, higher rewriting, and constructive semantics in homotopy type theory and concurrency models.

Abstract

We introduce a single-set axiomatisation of cubical $ω$-categories, including connections and inverses. We justify these axioms by establishing a series of equivalences between the category of single-set cubical $ω$-categories, and their variants with connections and inverses, and the corresponding cubical $ω$-categories. We also report on the formalisation of cubical $ω$-categories with the Isabelle/HOL proof assistant, which has been instrumental in developing the single-set axiomatisation.

Theorems & Definitions (38)

• Remark 2.1.2
• Example 2.1.5
• Example 2.1.6
• Lemma 2.1.7
• Example 2.1.8
• Example 2.2.5
• Lemma 2.2.7
• Lemma 2.2.10
• Lemma 2.2.11
• Lemma 2.3.4