Talk page

Title:
On Voevodsky's univalence principle

Speaker:
André Joyal

Abstract:
Abstract: The discovery of the "univalence principle" is a mark of Voevodsky's genius. Its importance for type theory cannot be overestimated: it is like the "induction principle" for arithmetic. I will recall the homotopy interpretation of type theory and the notion of univalent fibration. I will describe the connection between univalence and descent in higher toposes. I will sketch applications (direct and indirect) to homotopy theory (Blakers-Massey theorem, Goodwillie's calculus) and to higher topos theory (higher sheaves) [joint work with Mathieu Anel, Georg Biedermann and Eric Finster].

Link:
https://www.ias.edu/video/VoevodskyMemConf-2018/0911-AndreJoyal