| 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.