The Cayley-Dickson Construction in HoTT

0 views
Skip to first unread message

Ulrik Buchholtz

unread,
Oct 5, 2016, 2:33:24 PM10/5/16
to Homotopy Type Theory
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
Reply all
Reply to author
Forward
0 new messages