Computational Paths Form a Weak ω-Groupoid
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866908681914810368 |
|---|---|
| author | Ramos, Arthur F. de Veras, Tiago M. L. de Queiroz, Ruy J. G. B. de Oliveira, Anjolina G. |
| author_facet | Ramos, Arthur F. de Veras, Tiago M. L. de Queiroz, Ruy J. G. B. de Oliveira, Anjolina G. |
| contents | Lumsdaine (2010) and van den Berg-Garner (2011) proved that types in Martin-Löf type theory carry the structure of weak ω-groupoids. Their proofs, while foundational, rely on abstract properties of the identity type without providing explicit computational content for coherence witnesses. We establish an analogous result for computational paths -- an alternative formulation of equality where witnesses are explicit sequences of rewrites from the LNDEQ-TRS term rewriting system. Our main result is that computational paths on any type form a weak ω-groupoid with fully explicit coherence data. The groupoid operations -- identity, composition, and inverse -- are defined at every dimension, and the coherence laws (associativity, unit laws, inverse laws) are witnessed by concrete rewrite derivations rather than abstract existence proofs. The construction provides: (i) a proper tower of n-cells for all dimensions, with 2-cells as derivations between paths and higher cells mediating between lower-dimensional witnesses; (ii) explicit pentagon and triangle coherences built from the rewrite rules; and (iii) contractibility at dimensions $\geq 3$, ensuring all parallel higher cells are connected. The contractibility property is derived from the normalization algorithm of the rewrite system, grounding the higher-dimensional structure in concrete computational content. The entire construction has been formalized in Lean 4, providing machine-checked verification of the weak ω-groupoid structure. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_00657 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Computational Paths Form a Weak ω-Groupoid Ramos, Arthur F. de Veras, Tiago M. L. de Queiroz, Ruy J. G. B. de Oliveira, Anjolina G. Logic in Computer Science Lumsdaine (2010) and van den Berg-Garner (2011) proved that types in Martin-Löf type theory carry the structure of weak ω-groupoids. Their proofs, while foundational, rely on abstract properties of the identity type without providing explicit computational content for coherence witnesses. We establish an analogous result for computational paths -- an alternative formulation of equality where witnesses are explicit sequences of rewrites from the LNDEQ-TRS term rewriting system. Our main result is that computational paths on any type form a weak ω-groupoid with fully explicit coherence data. The groupoid operations -- identity, composition, and inverse -- are defined at every dimension, and the coherence laws (associativity, unit laws, inverse laws) are witnessed by concrete rewrite derivations rather than abstract existence proofs. The construction provides: (i) a proper tower of n-cells for all dimensions, with 2-cells as derivations between paths and higher cells mediating between lower-dimensional witnesses; (ii) explicit pentagon and triangle coherences built from the rewrite rules; and (iii) contractibility at dimensions $\geq 3$, ensuring all parallel higher cells are connected. The contractibility property is derived from the normalization algorithm of the rewrite system, grounding the higher-dimensional structure in concrete computational content. The entire construction has been formalized in Lean 4, providing machine-checked verification of the weak ω-groupoid structure. |
| title | Computational Paths Form a Weak ω-Groupoid |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2512.00657 |