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