Univalent Foundations

Members Seminar
Topic:Univalent Foundations
Speaker:Steve Awodey
Affiliation:Carnegie Mellon University; Member, School of Mathematics
Date:Monday, November 19
Time/Room:2:00pm - 3:00pm/S-101

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.