Hello, During the min 8 of the following video https://www.youtube.com/watch?v=3-E1SdSMipE 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. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.