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证明辅助器对立方ω-范畴进行形式化的成果，该工具在发现单集合公理过程中起到了关键作用。