Univalent Foundations Seminar

This talk is intended for a general audience. The recent discovery of an interpretation of constructive type theory into abstract homotopy theory has led to a new approach to foundations with both intrinsic geometric content and a computational implementation. In this setting, Vladimir Voevodsky has proposed new axiom for foundations with both geometric and logical significance: the Univalence Axiom. It captures formally a familiar practice of modern mathematics, namely the informal identification of isomorphic objects. Although UA is incompatible with conventional foundations, it is a powerful addition to homotopy type theory and forms the basis of the new Univalent Foundations Program. In this talk, I will explain homotopy type theory and the Univalence Axiom.