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

翻译：本文提出了一种包含连接与逆运算的立方体ω范畴的单集公理化体系。我们通过建立单集立方体ω范畴及其包含连接与逆运算的变体与对应立方体ω范畴之间的一系列等价关系，验证了这些公理的正确性。同时，我们报告了利用Isabelle/HOL证明辅助工具对立方体ω范畴进行形式化的工作，该形式化过程对发展单集公理化体系起到了关键作用。