Computational Paths Form a Weak ω-Groupoid
Arthur F. Ramos, Tiago M. L. de Veras, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
TL;DR
The paper constructs an explicit, computable weak $\omega$-groupoid structure on computational paths for any type, addressing the gap between abstract higher-categorical identifications and concrete computational witnesses. By employing the $\mathrm{LND}_{\mathrm{EQ}}$-TRS rewrite system and a canonical normalization through the canonicity axiom, it provides a full tower of cells with concrete 2-, 3-, and higher-dimensional coherence witnesses, including pentagon and triangle coherences, and proves contractibility in dimensions $\geq 3$. All results are formalized in Lean 4, ensuring machine-checked correctness and reproducibility. The framework aligns with classical identity-type results at low dimensions while delivering explicit, constructive coherence data at all higher levels, enabling applications in formalized higher-categorical reasoning within type theory. Overall, the work offers a principled bridge between syntax (computational paths) and semantics (weak $\omega$-groupoids) with practical formalization benefits.
Abstract
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.