Single-Set Cubical Categories and Their Formalisation with a Proof Assistant

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