Guillaume Brunerie: π₄(S³) in homotopy type theory
Time: Wed 2019-05-29 10.00 - 11.45
Lecturer: Guillaume Brunerie
Location: Room 16, building 5, Kräftriket, Department of Mathematics, Stockholm University
Abstract: In this talk I will present the main result of my PhD thesis, namely that π₄(S³) is isomorphic to Z/2Z in homotopy type theory. In order to translate this well known result from classical homotopy theory to homotopy type theory, several common constructions of homotopy theory (like the James construction, the Hopf invariant, the Gysin sequence) have to be redefined in a homotopy-invariant way using tools from homotopy type theory like higher inductive types and univalence. I will aim to make this talk accessible to both logicians and topologists.