A Topological Application of Labelled Natural Deduction

Abstract

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.

42 pages, 5 figures. arXiv admin note: text overlap with arXiv:1804.01413, arXiv:1803.01709, arXiv:1906.09107