45 citations · 190 across the 20 of their papers we have counts for
4 papers · 1 filter
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…
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…
Higher Catoids, Higher Quantales and their Correspondences
Cameron Calk, Philippe Malbos, Damien Pous +1
We introduce -catoids as generalisations of (strict) -categories and in particular the higher path categories generated by computads or polygraphs in higher-dimensional rewri…
Algebraic coherent confluence and higher globular Kleene algebras
Cameron Calk, Eric Goubault, Philippe Malbos +1
We extend the formalisation of confluence results in Kleene algebras to a formalisation of coherent confluence proofs. For this, we introduce the structure of higher globular Kleen…