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”. The formalization is taking place in the agda-unimath library.