2 papers
cs.LO2025
Cubical coherent confluence, -groupoids and the cube equation
Philippe Malbos, Tanguy Massacrier, Georg Struth
We study the confluence property of abstract rewriting systems internal to cubical categories. We introduce cubical contractions, a higher-dimensional generalisation of reductions…
cs.LO2024
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 -categories, including connections and inverses. We justify these axioms by establishing a series of equivalences between the…