One of the open problems in the development of synthetic homotopy
theory in homotopy type theory has been the construction of the
quaternionic and octonionic Hopf fibrations, arising from the H-space
structures on the three- and seven-sphere, respectively. Classically,
we can get these by considering the unit spheres in the quaternion and
octonion algebras, which we in turn can define using the
Cayley-Dickson construction. Here, we give a modified version of this
construction that works directly with the unit spheres, and in the
process we get the H-space structure on the three-sphere in HoTT (the
result has been formalized in Lean). This is based on joint work with
Egbert Rijke.
Links:
[1] https://www.mpim-bonn.mpg.de/taxonomy/term/39
[2] https://www.mpim-bonn.mpg.de/node/3444
[3] https://www.mpim-bonn.mpg.de/node/6459