Explicit computational paths in type theory

Abstract

The current work has three main objectives. The first one is the proposal of computational paths as a new entity of type theory. In this proposal, we point out the fact that computational paths should be seen as the syntax counterpart of the homotopical paths between terms of a type. We also propose a formalization of the identity type using computational paths. The second objective is the proposal of a mathematical structure fora type using computational paths. We show that using categorical semantics it is possible to induce a groupoid structure for a type and also a higher groupoid structure, using computational paths and a rewrite system. We use this groupoid structure to prove that computational paths also refutes the uniqueness of identity proofs. The last objective is to formulate and prove the main concepts and building blocks of homotopy type theory. We end this last objective with a proof of the isomorphism between the fundamental group of the circle and the group of the integers.