On Voevodsky's univalence principle

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].