Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Hi everyone! I’m back from a 2-week vacation without Internet access. It’ll take me a little while to catch up on everything, but just so you know, I’m here again now….
Good to hear that you are back!
I was in Pittsburgh last week and spoke with some of the HoTT people there. Only through this conversation has it become clear to me that the HoTT derivation of
that you had posted to the blog a while back is regarded as a big achievement in the field! I hear that Joyal is currently following a project for next computing . Sounds like this is something that will keep HoTTists busy for a while. :-)
Welcome back! I figured that you were just hunkering down to research and avoiding getting distracted by internet stuff, forgetting that I too take internet-free vacations on occasion. :-)
the HoTT derivation of that you had posted to the blog a while back is regarded as a big achievement in the field!
That’s nice to hear; I haven’t actually talked to any of them in person since the HoTT Oberwolfach meeting. (-: I wonder what approach Joyal is taking to . The “obvious” approach to me is to construct the Hopf fibration and prove the homotopy long exact sequence of a fibration, but it’s not obvious to me how to identify the total space of the Hopf fibration as being (or, at least, 2-simply-connected). I guess that that approach would also first involve proving at least for small , which one could maybe do with the Freudenthal suspension theorem.
Yes, apparently Joyal is going via the Hopf fibration. But that’s already all I have heard about it. (Apart from giving a talk to the whole group, I mostly chatted with Krzysztof Kapulkin, who told me these things.)
1 to 5 of 5