2018/03/02 by Arthur Ramos, Ramos, Arthur F., Ruy J. G. B. de Queiroz +5
Computer Science · Mathematics · #Algebraic Geometry and Number Theory #FOS: Computer and information sciences #Homotopy and Cohomology in Algebraic Topology #Logic in Computer Science (cs.LO) #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1803.01709
openalex publication_date 2018/03/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
The treatment of equality as a type in type theory gives rise to an interesting type-theoretic structure known as `identity type'. The idea is that, given terms a,b of a type A, one may form the type IdA(a,b), whose elements are proofs that a and b are equal elements of type A. A term of this type, p : IdA(a,b), makes up for the grounds (or proof) that establishes that a is indeed equal to b. Based on that, a proof of equality can be seen as a sequence of substitutions and rewrites, also known as a `computational path'. One interesting fact is that it is possible to rewrite computational paths using a set of reduction rules arising from an analysis of redundancies in paths. These rules were mapped by De Oliveira in 1994 in a term rewrite system known as LNDEQ-TRS. Here we use computational paths and this term rewrite system to work with path spaces. In homotopy type theory, the main technique used to define path spaces is the code-encode-decode approach. Our objective is to propose an alternative approach based on the theory of computational paths. We believe this new approach is simpler and more straightforward than the code-encode-decode one. We then use our approach to obtain two important results of homotopy type theory: the construction of the path space of the naturals and the calculation of the fundamental group of the circle.