Construction of the Hopf fibration in Homotopy Type Theory, using the HoTT library for Coq.
You will need to install the HoTT library for Coq.
I recommend using the hoqide script to run the familiar CoqIDE with all required dependencies preloaded.
Then you can load the script Homework.v as usual.
You can also access the HTML version of the script rendered with coqdoc.