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

2024/01/19 by Malbos, Philippe, Massacrier, Tanguy, Struth, Georg
#03B35 #18N30 #68Q42 #68V15 #Category Theory (math.CT) #FOS: Computer and information sciences #FOS: Mathematics #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2401.10553

Abstract

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

Related

• Cubical (omega,p)-categories
• Multiple categories: the equivalence of a globular and a cubical approach
• Aspects of Cubical Higher Category Theory
• Varieties of Cubical Sets
• A co-reflection of cubical sets into simplicial sets with applications to model structures