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

Philippe Malbos, Tanguy Massacrier, Georg Struth

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…