Ulrik Buchholtz (TU Darmstadt): The Cayley-Dickson construction in homotopy type theory

The classical Cayley-Dickson construction produces a sequence of algebras, including the quaternion and octonion algebras, from which we get H-space structures on the three- and seven-spheres by taking unit spheres, and hence we get the quaternionic and octonionic Hopf fibrations. I will describe a version of the Cayley-Dickson construction that works directly with the unit spheres, using homotopy type theory. Homotopy type theory can (conjecturally) be seen as an internal language to reason about higher toposes, giving rise to a kind of synthetic homotopy theory. Indeed, this version of the Cayley-Dickson construction works in any higher topos.