cs.LO math.AT
A Topological Application of Labelled Natural Deduction. We use a labelled deduction system based on the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type. We also define a term rewriting system that is used to make computations between these computational paths, establishing equalities between equalities. We then proceed to show the main result here using this system to obtain the calculation of the fundamental group of the circle, of the torus and the real projective plane.