# The Cayley-Dickson construction in HoTT

Our paper on the Cayley-Dickson construction in HoTT, which is joint work with Ulrik Buchholtz, has been submitted to the Arxiv:

The Cayley-Dickson construction in Homotopy Type Theory

In this paper, we formalize the H-space structure on the 3-sphere. One can think of the 3-sphere as the unit-sphere in the quaternions. Since the quaternions form a normed division algebra, multiplication of quaternions can be used to obtain the H-space structure on the 3-sphere. However, these methods are not directly available in HoTT.

Instead, we construct this H-space structure using only homotopy invariant methods. One consequence of this, is that our methods should be applicable to get the H-space structure of the 3-sphere in any setting for homotopy theory where homotopy pushouts are available.

Given the H-space structure on the 3-sphere, we also obtain via the Hopf-construction a fibration $S^3 \hookrightarrow{} S^7 \twoheadrightarrow{} S^4$. And since inclusion $S^3 \hookrightarrow{} S^7$ in the Hopf-construction is null-homotopic, we get embeddings $\pi_k(S^7) \to{} \pi_k(S^4)$ of homotopy groups, for any $k$. In particular, since $\pi_7(S^7)=\mathbb{Z}$, we get an element of $\pi_7(S^4)$ of infinite order.