Eckmann-Hilton and the Hopf Fibration in Homotopy Type Theory
Date:
Confrence website: https://hott.github.io/HoTT-2023/
This talk presents the results of my honors thesis. In the talk I define a map $\mathbb{S}^3 \to \mathbb{S}^2$ using the Eckmann-Hilton argument (that sends the generating 3-loop of $\mathbb{S}^3$ to a 3-loop in $\mathbb{S}^2$ that was constructed using the Eckmann-Hilton argument). Then we present a method for characterizing the fiber of this map. This method can be seen as a generalization of methods used to characterize the loop space of a type. Here are the slides from the talk available for download: sildes.