Our paper on the Cayley-Dickson construction in HoTT, which is joint work with Ulrik Buchholtz, has been submitted to the Arxiv:
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 . And since inclusion in the Hopf-construction is null-homotopic, we get embeddings of homotopy groups, for any . In particular, since , we get an element of of infinite order.