Showing changes from revision #2 to #3:
Added | Removed | Changed
In classical algebraic topology we have four Hopf fibrations (of spheres):
These can be constructed in HoTT as part of a more general construction:
A H-space structure on a pointed (connected?) type gives a fibration over via the hopf construction. This fibration can be written classically as: where is the join of and . This is all done in the HoTT book. Note that can be written as a homotopy pushout , and there is a lemma in the HoTT book allowing you to construct a fibration on a pushout (the equivalence needed is simply the multiplication from the H-space ).
Thus the problem of constructing a hopf fibration reduces to finding a H-space structure on the spheres: the , , and .
For this is a trivial exercise and it is in the book.
For Lumsdaine gave the construction in 2012 and Brunerie proved it was correct in 2013.
For Buchholtz-Rijke 16 solved this through a homotopy theoretic version of the Cayley-Dickson construction.
For this is still an open problem.
It is still an open problem to show that these are the only spaces to have a H-space structure.