In this thesis, we study the Hopf fibration in homotopy type theory. We present the synthetic interpretation of types as spaces and identifications as paths, and develop the notions of transport, homotopy, equivalence, connectedness, and homotopy groups. Using higher inductive types, we define the circle, suspensions, spheres, pushouts, and joins. With the help of the $H$-structure on the circle and the univalence axiom, we construct a type family over the sphere $\mathbb{S}^2$ whose distinguished fibre is $\mathbb{S}^1$. Using the flattening lemma, we show that its total space is equivalent to the sphere $\mathbb{S}^3$, thus obtaining the Hopf fibration
$$\mathbb{S}^1 \longrightarrow \mathbb{S}^3 \longrightarrow \mathbb{S}^2.$$ We compute the fundamental group of the circle and show that $\pi_1(\mathbb{S}^1)\simeq\mathbb{Z}$, while its higher homotopy groups are trivial. Using the long exact sequence of the Hopf fibration, we then derive $$\pi_2(\mathbb{S}^2)\simeq\mathbb Z$$ and $\pi_n(\mathbb{S}^2)\simeq\pi_n(\mathbb{S}^3)$ for every $n\geq 3$.
|
