Skip to main content
To KTH's start page To KTH's start page

Guillaume Brunerie: π₄(S³) in homotopy type theory

Time: Wed 2019-05-29 10.00 - 11.45

Location: Room 16, building 5, Kräftriket, Department of Mathematics, Stockholm University

Participating: Guillaume Brunerie

Export to calendar

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.