  The goal of this thesis is to prove that $\pi_4(S^3) \simeq
\mathbb{Z}/2\mathbb{Z}$ in homotopy type theory. In particular it is a
constructive and purely homotopy-theoretic proof. We first recall the basic
concepts of homotopy type theory, and we prove some well-known results about
the homotopy groups of spheres: the computation of the homotopy groups of the
circle, the triviality of those of the form $\pi_k(S^n)$ with $k < n$, and the
construction of the Hopf fibration. We then move to more advanced tools. In
particular, we define the James construction which allows us to prove the
Freudenthal suspension theorem and the fact that there exists a natural number
$n$ such that $\pi_4(S^3) \simeq \mathbb{Z}/n\mathbb{Z}$. Then we study the
smash product of spheres, we construct the cohomology ring of a space, and we
introduce the Hopf invariant, allowing us to narrow down the $n$ to either $1$
or $2$. The Hopf invariant also allows us to prove that all the groups of the
form $\pi_{4n-1}(S^{2n})$ are infinite. Finally we construct the Gysin exact
sequence, allowing us to compute the cohomology of $\mathbb{C}P^2$ and to prove
that $\pi_4(S^3) \simeq \mathbb{Z}/2\mathbb{Z}$ and that more generally
$\pi_{n+1}(S^n) \simeq \mathbb{Z}/2\mathbb{Z}$ for every $n \ge 3$.
