Authors apply labeled deduction with computational paths and Seifert-Van Kampen theorem to compute fundamental groups of Klein bottle K², torus T², and two-holed torus M₂.
On the Identity Type as the Type of Computational Paths
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
abstract
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. Our approach enjoys the fact that our elimination rule is easy to understand and use. We make this point clear constructing terms of some relevant types using our proposed elimination rule. We also show that the identity type, as defined by our approach, induces a groupoid structure. This result is on par with the fact that the traditional identity type induces a groupoid, as exposed by Hofmann \& Streicher (1994).
fields
cs.LO 1years
2019 1verdicts
UNVERDICTED 1representative citing papers
citing papers explorer
-
An alternative approach to the calculation of fundamental groups based on labeled natural deduction
Authors apply labeled deduction with computational paths and Seifert-Van Kampen theorem to compute fundamental groups of Klein bottle K², torus T², and two-holed torus M₂.