During the min 8 of the following video
the mathematician Prof. Eric Weinstein (Harvard) claimed that the Hopf fibrations is the most important object in the universe. According to the principle
types (in the sense of type theory) = homotopy types (in the sense of topology)
the Hopf fibrations are a type in the sense of type theory. My question is: What does this type means from the point of view of computer science? Are there some possible concrete applications of Hopf fibrations to proof assistants and programming languages via HoTT?
Kind Regards,
José M.