From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Wed, 5 Oct 2016 11:33:23 -0700 (PDT) From: Ulrik Buchholtz To: Homotopy Type Theory Message-Id: <89d205a9-f08b-4b01-98d1-002dd76041c0@googlegroups.com> Subject: The Cayley-Dickson Construction in HoTT MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_59_38214202.1475692403647" ------=_Part_59_38214202.1475692403647 Content-Type: multipart/alternative; boundary="----=_Part_60_511451286.1475692403647" ------=_Part_60_511451286.1475692403647 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit 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 ------=_Part_60_511451286.1475692403647 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
As previously announced at the MPIM workshop in Bonn in Fe= bruary, and at the TYPES meeting in Novi Sad in May, Egbert and I have a ve= rsion of the Cayley-Dickson construction in HoTT, which we've so far us= ed to construct the H-space structure on S^3.

Now the pa= per is available on the arXiv here:=C2=A0https://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:=C2=A0https://egbertrijke.com/2016/10/05/the-cayley-di= ckson-construction-in-hott/

Cheers,
Ulri= k
------=_Part_60_511451286.1475692403647-- ------=_Part_59_38214202.1475692403647--