Thierry Coquand

Type Theory and Univalent Foundation

This will be an introduction to the Univalent Foundation Program, starting from┬áChurch’s simple type theory, Curry-Howard propositions-as-types principle, the distinction between intensional and extensional equality, and then Voevodsky’s stratification of types, following the complexity of their equality, and the Axiom of Univalence. I will then try to present some consequences of this approach for the formalization of mathematics.