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 finding the single-set axioms.

翻译：我们引入了包括连接和逆在内的立方体ω-范畴的单集合公理化。通过建立单集合立方体ω-范畴范畴与其带连接和逆的变体以及相应立方体ω-范畴之间的一系列等价关系，我们验证了这些公理的合理性。我们还报告了使用Isabelle/HOL证明助理对立方体ω-范畴进行形式化的过程，该形式化在发现单集合公理中起到了关键作用。