Cubical coherent confluence, $ω$-groupoids and the cube equation
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866917137777426432 |
|---|---|
| author | Malbos, Philippe Massacrier, Tanguy Struth, Georg |
| author_facet | Malbos, Philippe Massacrier, Tanguy Struth, Georg |
| contents | 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 $λ$-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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_16852 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Cubical coherent confluence, $ω$-groupoids and the cube equation Malbos, Philippe Massacrier, Tanguy Struth, Georg Logic in Computer Science Category Theory 03B35, 68Q42, 18N30 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 $λ$-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. |
| title | Cubical coherent confluence, $ω$-groupoids and the cube equation |
| topic | Logic in Computer Science Category Theory 03B35, 68Q42, 18N30 |
| url | https://arxiv.org/abs/2511.16852 |