用计算路径计算同伦类型论中的基本群
On the Calculation of Fundamental Groups in Homotopy Type Theory by Means of Computational Paths
摘要：
同伦类型论中最有趣的实体之一是单位类型。它产生了一个有趣的解释的平等，因为人们可以语义解释之间的平等两项相同类型的收集同伦路径之间的点相同的空间。由于这只是一种语义解释，最近德奎罗斯、拉莫斯和德奥利维拉提出了在同伦类型论的语法中加入路径。在这些作品中，作者提出了一个被称为“计算路径”的实体，由De Queiroz和Gabbay在1994年提出，并表明它可以用来形式化的身份类型。我们已经发现，有可能使用这些计算路径作为工具，以实现一个中心结果的代数拓扑和同伦类型论：计算基本群的表面。我们回顾了计算路径的概念和$LND_{EQ}-TRS$，这是一个长期重写系统提出的De Oliveira在1994年计算路径之间的映射冗余。然后，我们继续计算基本群的圆，圆柱，M{<$}bius带，环面和真正的射影平面。此外，我们表明，使用的计算路径，使这些计算简单和直接，而同样的结果是很难获得使用传统的编码-编码-解码方法的同伦类型论。
英文摘要：
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{ö}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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
