Topological Semantics for Scoped Computational Paths

Abstract

Computational paths record the steps of an equality derivation. We give them a topological semantics that distinguishes derivable rewrites from arbitrary homotopies. Coherent representatives pair traces with paths homotopic to their realizations. We compare a topology retaining the entire trace with one observing only endpoints, length, and paths. Quotienting by the declared rewrites gives a groupoid. Multiplication is continuous when composable pairs carry the quotient topology inherited from composable representatives. This topology can differ from the usual subspace topology on pairs of quotient arrows. We characterize when they agree, give compact-Hausdorff and discrete sufficient conditions, and use the Hawaiian earring to exhibit a failure of agreement. The comparison with geometric homotopy classes is injective exactly when the presentation is geometrically complete. Normal-form certificates give a criterion for completeness. In the universal presentation, all paths are primitive steps and all endpoint-fixed homotopies are allowed rewrites; its quotient recovers the quotient-topologized fundamental groupoid. Circle and torus examples recover the classical based-loop classifications by $\mathbb Z$ and $\mathbb Z^2$. A Lean development supports the construction. A focused Lean 4.32.0 result registered in Palomar covers the topology comparison, additive circle and torus classifications, and a conditional Hawaiian-earring obstruction transfer. We distinguish that result from the earlier Lean 4.24.0 development and from the mathematical exposition.