Computational paths - a weak groupoid

On the basis of a labelled deduction system (LND$_{ED-}$TRS), we demonstrate how to formalize the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type. This has allowed us to carry out a formal counterpart to equality between paths which is dealt with in homotopy theory, but this time with an approach using the device of term-rewriting paths. Using such formal calculus dealing with paths, we construct the fundamental groupoid of a path-connected $ X $ type and we define the concept of isomorphism between types. Next, we show that the computational paths determine a weak category, which will be called $ \mathcal {C}_{paths} $. Finally, we show that the weak category $ \mathcal {C}_{paths} $ determines a weak groupoid.

Automated summary

This paper demonstrates how to formalize the concept of computational paths as equalities between two terms of the same type using a labelled deduction system. With this formalization, the fundamental groupoid of a path-connected type and the concept of isomorphism between types are constructed. It is also shown that computational paths determine a weak category and a weak groupoid.