Computational Paths Form a Weak {\omega}-Groupoid

TL;DR

This paper demonstrates that computational paths in type theory form a weak ω-groupoid with explicit coherence data, providing a concrete, formalized, and machine-verified structure grounded in rewrite systems.

Contribution

It establishes a weak ω-groupoid structure for computational paths with explicit coherence witnesses, extending prior abstract results to a computationally explicit framework.

Findings

Computational paths form a weak ω-groupoid with explicit coherence data.

The structure is formalized and verified in Lean 4.

Higher cells and coherence laws are constructed from rewrite rules.

Abstract

Lumsdaine (2010) and van den Berg-Garner (2011) proved that types in Martin-L\"of type theory carry the structure of weak {\omega}-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 {\omega}-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 {\omega}-groupoid structure.