As previously announced at the MPIM workshop in Bonn in February, and at the TYPES meeting in Novi Sad in May, Egbert and I have a version of the Cayley-Dickson construction in HoTT, which we've so far used to construct the H-space structure on S^3.

Now the paper is available on the arXiv here: https://arxiv.org/abs/1610.01134

(The formalization has been a part of the Lean HoTT library for a while.)

Also, Egbert has written a short blog post here: https://egbertrijke.com/2016/10/05/the-cayley-dickson-construction-in-hott/

Cheers,

Ulrik