On Computational Paths and the Fundamental Groupoid of a Type

TL;DR

This paper explores the use of computational paths within type theory to construct fundamental groupoids, linking syntactic entities to homotopical interpretations and extending to higher levels.

Contribution

It introduces a novel syntactic approach to constructing fundamental groupoids of types using computational paths, bridging syntax and homotopy theory.

Findings

Constructed a fundamental groupoid for any type using computational paths.

Extended the framework to higher-level fundamental groupoids.

Demonstrated the connection between computational paths and homotopical semantics.

Abstract

The main objective of this work is to study mathematical properties of computational paths. Originally proposed by de Queiroz \& Gabbay (1994) as `sequences of rewrites', computational paths can be seen as the grounds on which the propositional equality between two computational objects stand. Using computational paths and categorical semantics, we take any type $A$ of type theory and construct a groupoid for this type. We call this groupoid the fundamental groupoid of a type $A$, since it is similar to the one obtained using the homotopical interpretation of the identity type. The main difference is that instead of being just a semantical interpretation, computational paths are entities of the syntax of type theory. We also expand our results, using computational paths to construct fundamental groupoids of higher levels.