The Cayley-Dickson Construction in Homotopy Type Theory
Egbert Rijke, Ulrik Buchholtz
Received October 25th 2016. Published online November 8th 2018.
Abstract: We define in the setting of homotopy type theory an H-space structure on $\Bbb S^3$. Hence we obtain a description of the quaternionic Hopf fibration $\Bbb S^3 \hookrightarrow \Bbb S^7 \twoheadrightarrow \Bbb S^4 $, using only homotopy invariant tools. A side benefit is that the construction applies to more general $\infty$-categories than that of spaces.
