* The Cayley-Dickson Construction in HoTT
@ 2016-10-05 18:33 Ulrik Buchholtz
0 siblings, 0 replies; only message in thread
From: Ulrik Buchholtz @ 2016-10-05 18:33 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 551 bytes --]
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
[-- Attachment #1.2: Type: text/html, Size: 678 bytes --]
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2016-10-05 18:33 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2016-10-05 18:33 The Cayley-Dickson Construction in HoTT Ulrik Buchholtz
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).