Cubical coherent confluence, $\omega$-groupoids and the cube equation

TL;DR

This paper develops a categorical framework for analyzing rewriting systems using cubical structures, proving fundamental theorems and deriving the cube law, leading to new insights into higher-dimensional algebraic systems.

Contribution

It introduces cubical contractions and constructs cubical resolutions, providing categorical proofs of key rewriting theorems and connecting to the cube law in lambda calculus and Garside theory.

Findings

Established cubical proofs of Newman's lemma, Church-Rosser theorem, and Squier's coherence theorem.

Showed that convergent rewriting systems generate acyclic cubical groupoids.

Derived the cube law within a categorical framework.

Abstract

We study the confluence property of abstract rewriting systems internal to cubical categories. We introduce cubical contractions, a higher-dimensional generalisation of reductions to normal forms, and employ them to construct cubical polygraphic resolutions of convergent rewriting systems. Within this categorical framework, we establish cubical proofs of fundamental rewriting results -- Newman's lemma, the Church-Rosser theorem, and Squier's coherence theorem -- via the pasting of cubical coherence cells. We moreover derive, in purely categorical terms, the cube law known from the $\lambda$-calculus and Garside theory. As a consequence, we show that every convergent abstract rewriting system freely generates an acyclic cubical groupoid, in which higher-dimensional generators can be replaced by degenerate cells beyond dimension two.