  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 $a,b$ of a type $A$, one may form the type $Id_{A}(a,b)$,
whose elements are proofs that $a$ and $b$ are equal elements of type $A$. A
term of this type, $p : Id_{A}(a,b)$, makes up for the grounds (or proof) that
establishes that $a$ is indeed equal to $b$. Based on that, a proof of equality
can be seen as a sequence of substitutions and rewrites, also known as a
`computational path'. One interesting fact is that it is possible to rewrite
computational paths using a set of reduction rules arising from an analysis of
redundancies in paths. These rules were mapped by De Oliveira in 1994 in a term
rewrite system known as $LND_{EQ}-TRS$. Here we use computational paths and
this term rewrite system to develop the main foundations of homotopy type
theory, i.e., we develop the lemmas and theorems connected to the main types of
this theory, types such as products, coproducts, identity type, transport and
many others. We also show that it is possible to directly construct path spaces
through computational paths. To show this, we construct the natural numbers and
the fundamental group of the circle, showing results connected to these
structures.
