# 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

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.