In topology, a branch of mathematics, two continuous functions from one topological space to another are called homotopic if one can be "continuously deformed" into the other, such a deformation being called a homotopy between the two functions. The HoTT is a new field of study that tries to analyze the classical homotopy from the perspective of type theory. In other words, we want to investigate the syntax of the classical homotopy. The central new idea in HoTT is that types are spaces in homotopy theory, or higher-dimensional groupoids in category theory. Consider points in a space, they can enjoy the morphism property; and so are paths; homotopies; homotopies between homotopies, and so an. This is called the $\infty$-groupoid.
In type theory, we have a dependent type, the identity type $x ={A} y$ given two inhabitants of $A$: $x,y:A$. This is a path between two points $x$ and $y$ in the space $A$. Two paths $p,q:x={A} y$ with the same start and end point are said to be parallel, in which case an element $r:p={x={A}}q$ can be thought of as a homotopy, or simply morphism between morphisms.
The identity type enjoys the symmetry property which says
$$ \prod_{A:\mathcal{U}}\prod_{x,y :A} (x={A}y) \to (y={A}x). $$
Equivalently, we say that “paths can be reversed”. The above is denoted $p \mapsto p^{-1}$, or $\mathsf{refl} \equiv \mathsf{refl}^{-1}$. The proof should be an inhabitant of the above dependent function type.
Proof. First obverse that the only inhabitant of the identity type is $\mathsf{refl}{A}:x ={A}x$ for some $x$. Thus we easily obtain that $\prod_{z:A} \mathsf{refl}{z}$ ’s type is $(z:A) \to (y={A}x)[y \mapsto z, x \mapsto z, p \to z ={A} z]$ where $p:x={A}y$. By induction rule we know that $ind_{=}(x, y, p, \mathsf{refl}{x})$ is the given type. $\square$ We can further define $p^{-1}\equiv ind{=}(x,y,p,\mathsf{refl}_z)$.
Similarly, we can “concatenate” paths from existing paths, as long as they have connecting point:
For every type $A:\mathcal{U}$ and $x,y,z:A$, we have
$$ (x = y) \to (y = z) \to (x = z), $$
written $p \mapsto q \mapsto p \circ q$ such that $\mathsf{refl}{x} \circ \mathsf{refl}{x} \equiv \mathsf{refl}_x$ for every $x:A$.
Proof. Straightforward pattern match on $(x=y)$ and $(y=z)$. $\square$
It is often considered trivial that $a = a$ because it is just reflexivity. However, in HoTT, it $a=a$ might be a path starting from $a$ and ending at $a$. We call such structure loop space $\Omega(A,a)$ to be the type $a = _{A} a$. Let us consider the 2-dimensional loop space $\Omega^2(A,a)$ whose type is $\mathsf{refl} = _{\mathsf{refl}}\mathsf{refl}$. While it is now a loop space, is again a “higher group”, it now also has some additional structure resulting from the fact that its elements are 2-dimensional loops between 1-dimensional loops:
Eckmann–Hilton: The composition operation on the second loop space
$$ \Omega^2 \times \Omega^2 \to \Omega^2 $$
is commutative: $\alpha \circ \beta = \beta \circ \alpha$ for any $\alpha, \beta: \Omega^2$.