The Cayley-Dickson Construction in Homotopy Type Theory

Ulrik Buchholtz, Egbert Rijke

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^3\hookrightarrow…