Talk page
Title:
On Voevodsky's univalence principle
Speaker:
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: