Homotopy Type Theory and Univalent Foundations of Mathematics

Steve Awodey (CMU/MCMP) gives a talk at the MCMP Colloquium (13 June, 2012) titled "Homotopy Type Theory and Univalent Foundations of Mathematics". Abstract: Recent advances in foundations of mathematics have led to some developments that are significant for the philosophy of mathematics, particularly structuralism. The discovery of an interpretation of constructive type theory into homotopy theory suggests a new approach to the foundations of mathematics with both intrinsic geometric content and a computational implementation. In this setting, leading homotopy theorist Vladimir Voevodsky has proposed new axiom for foundations with both geometric and logical significance: the Univalence Axiom. It captures the familiar aspect of informal mathematical practice, according to which one can identify isomorphic objects. While it is incompatible with conventional foundations, it is a powerful addition to homotopy type theory, and forms the basis of the new Univalent Foundations Program.