English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

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

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