Formalizing Eckmann-Hilton and the Hopf Fibration in Homotopy Type Theory
I have been working towards formalizing the results of my honors thesis, “Eckmann-Hilton and the Hopf Fibration in Homotopy Type Theory”. I aim to have this fully formalized by the end of 2023, or early 2024. The formalization uses the agda-unimath library.