Topological Semantics for Scoped Computational Paths
Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira, Tiago M. L. de Veras
cs.LO
Aug 4, 2026 · v1
math.AT
TL;DR
A Lean 4.24.0 development checks the theorem package for a topological semantics of scoped computational paths.
Abstract
Computational paths record equality as explicit finite traces of primitive steps. We give a topological semantics for a scoped rewrite presentation whose steps have continuous geometric realizations and whose named rewrites carry endpoint-fixed homotopies. For every presentation we construct a quotient arrow space with a canonical final-domain groupoid structure: multiplication is continuous on the quotient of explicitly composable representatives. We prove an exact four-way criterion for this final composable topology to agree with the ordinary pullback topology, together with a compact-Hausdorff sufficient condition. Thus the unconditional construction exposes, rather than hides, the product-quotient issue in ordinary topological groupoids. The realization map to geometric homotopy classes is a continuous groupoid morphism and is faithful exactly under a separate geometric-completeness condition. In the universal presentation, a continuous section identifies the coherent-path quotient homeomorphically with the usual quotient-topologized fundamental groupoid. We then give finite-generator circle and genuine torus examples, with winding-based normal forms and classifications by Z and Z^2. A Lean 4.24.0 development checks the theorem package; the mathematical presentation is independent of the implementation.
Problem
Computational paths record equality as explicit finite traces of primitive steps, but a topological interpretation should be sound without identifying every trace whose realization is homotopic. Passing to rewrite classes creates a product-quotient problem: continuity of concatenation on representatives does not automatically imply continuity of multiplication for the ordinary pullback topology.
Approach
A scoped rewrite presentation is given whose steps have continuous geometric realizations and whose named rewrites carry endpoint-fixed homotopies. A quotient arrow space is constructed with a canonical final-domain groupoid structure, taking the quotient of explicitly composable representatives so multiplication is continuous. The ordinary pullback topology is compared as a separate theorem, and realization is shown to be a continuous groupoid morphism. Finite-generator circle and torus examples are worked out with winding-based normal forms.
Results
An exact four-way criterion is proven for when the final composable topology agrees with the ordinary pullback topology, plus a compact-Hausdorff sufficient condition. For the universal presentation a continuous section identifies the coherent-path quotient homeomorphically with the usual fundamental groupoid, and circle and torus examples are classified by Z and Z^2. A Lean 4.24.0 development checks the theorem package.
