news from Bonn

[Steve Awodey]

[Mark Farrell]

Quoi?

On Sunday, February 14, 2016 at 10:39:12 PM UTC, Steve Awodey wrote:

[Egbert Rijke]

Guillaume gave a wonderful presentation this afternoon of his proof in HoTT that \pi_4(S^3) is Z/2Z, using the James construction, the Hopf invariant of the Hopf fibration and the Gysin sequence. Synthetic homotopy theory at its best!

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Andrej Bauer]

Does this mean he actually computed the Brunerie number? What is its value?

[Guillaume Brunerie]

It depends what you mean by "compute".

I computed it in the mathematical sense, in that I provided a proof that it is equal to 2.
I didn't compute it in the type theoretical sense, which would mean taking the term n : N, applying some kind of normalization procedure, and getting 2 in the end.

[Michael Shulman]

You shouldn't have to ask what its value is: if he computed it in the sense of proving it equal to a canonical nat, then it must be 2 since that's what it is in the classical model.

This is awesome; I look forward to hearing/reading details.

[Dan Christensen]

This reminds me of a question I've had for a while: is there any reason
to expect that all models of HoTT have the same homotopy groups of
spheres? Of course, if we can compute them in HoTT then they must agree
in all models and so must match the classical homotopy groups of
spheres. And we now know that in several cases we can compute them
in HoTT, so it's a natural conjecture that there's a meta-result
that says that they must all match the classical homotopy groups of
spheres. But this seems surprising to me. Has anyone tried to find
models with unexpected homotopy groups of spheres?

Dan

[Michael Shulman]

In my opinion this is one of the most fascinating open problems of HoTT, which I've been pondering for a while. My bet is still on them being the same in all models, based on a higher-category-theorist's intuition that they are just shadows of the higher coherence structure of an infinity-groupoid, which ought to be completely constructive. However, it's intriguing that the most powerful methods for computing them in classical homotopy theory use nonconstructive facts, like that every vector space over a field is projective. At the moment we haven't even managed to prove in HoTT that all homotopy groups of spheres are finitely generated. But if some of them are 'universal', like pi_n(S^n) and pi_(n+1)(S^n), and some aren't, then what distinguishes the universal ones from the contingent ones?

[Mark Farrell]

Hmm, cool. However, to my knowledge, the homotopy type theory book already mentions that Brunerie calculated \pi_4(S^3)? I believe I've also heard that he gave a proof at a past Oxford workshop?
If that is the case, what is new with this proof? Is it new in that it is a constructive proof that \pi_4(S^3) = Z/nZ for some n, where n is 'implicit', so to speak? (That would be awesome, if I understand correctly?)

[Daniel R. Grayson]

Yes, the statement is stronger now, with n replaced by 2.