On Voevodsky's univalence principle

André Joyal
Université du Québec á Montréal
September 11, 2018
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.