The Cayley-Dickson Construction in Homotopy Type Theory

We define in the setting of homotopy type theory an H-space structure on $mathbb S^3$. Hence we obtain a description of the quaternionic Hopf fibration $mathbb S^3hookrightarrowmathbb S^7twoheadrightarrowmathbb S^4$, using only homotopy invariant tools.