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.
Just announced on the homotopy type theory list by Awodey (cryptically, using a blurry photo [1]) and Rijke (in some more detail):
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!
[1] https://plus.google.com/+DavidRoberts/posts/aHPwEompKhS (broken link)
1 to 1 of 1