3 citations · 3 across the 1 of their papers we have counts for
4 papers · 1 filter
An alternative approach to the calculation of fundamental groups based on labeled natural deduction
Tiago M. L. de Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz +1
In this work, we use a labelled deduction system based on the concept of computational paths (sequence of rewrites) as equalities between two terms of the same type. We also define…
On the Calculation of Fundamental Groups in Homotopy Type Theory by Means of Computational Paths
Tiago Mendonça Lucena de Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz +1
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 interp…
On the Use of Computational Paths in Path Spaces of Homotopy Type Theory
Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira +1
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 of a type …
On the Identity Type as the Type of Computational Paths
Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
We introduce a new way of formalizing the intensional identity type based on the fact that a entity known as computational paths can be interpreted as terms of the identity type. O…