On the Calculation of Fundamental Groups in Homotopy Type Theory by Means of Computational Paths

TL;DR

This paper demonstrates how computational paths in homotopy type theory can be effectively used to compute fundamental groups of various surfaces, simplifying the process compared to traditional methods.

Contribution

It introduces the use of computational paths for calculating fundamental groups within homotopy type theory, providing a more straightforward approach.

Findings

Successfully computed fundamental groups of key surfaces

Showed computational paths simplify homotopy type theory calculations

Compared approach with traditional code-encode-decode method

Abstract

One of the most interesting entities of homotopy type theory is the identity type. It gives rise to an interesting interpretation of the equality, since one can semantically interpret the equality between two terms of the same type as a collection of homotopical paths between points of the same space. Since this is only a semantical interpretation, the addition of paths to the syntax of homotopy type theory has been recently proposed by De Queiroz, Ramos and De Oliveira . In these works, the authors propose an entity known as `computational path', proposed by De Queiroz and Gabbay in 1994, and show that it can be used to formalize the identity type. We have found that it is possible to use these computational paths as a tool to achieve one central result of algebraic topology and homotopy type theory: the calculation of fundamental groups of surfaces. We review the concept of computational paths and the $LND_{EQ}-TRS$, which is a term rewriting system proposed by De Oliveira in 1994 to map redundancies between computational paths. We then proceed to calculate the fundamental group of the circle, cylinder, M{\"o}bius band, torus and the real projective plane. Moreover, we show that the use of computational paths make these calculations simple and straightforward, whereas the same result is much harder to obtain using the traditional code-encode-decode approach of homotopy type theory.