[Alta-Logic] Friday: Awodey on Homotopy Type Theory in the Math Colloquium

[Richard Zach]

Date & Time: Friday, October 3, 2014 from 2:00pm to 3:00pm.
Location: MS 211
Speaker: Prof. Steve Awodey (Carnegie Mellon University)
Title: Homotopy Type Theory

Abstract. Homotopy type theory is a homotopical interpretation of a 
system of formal logic, providing a new framework for the foundations of 
mathematics with intrinsic homotopical content and a computational 
implementation. It forms the basis of the Univalent Foundations program, 
which was the subject of a recent special year at IAS. In this survey 
talk, I will introduce this system and show how it can be used to give 
new logical proofs of some classical theorems from algebraic topology, 
making use of the new ideas of higher inductive types and the univalence 
axiom.

Biography. Dr. Steve Awodey is an internationally recognized researcher 
in the areas of category theory and logic, and has also written on the 
philosophy of mathematics. He received his Ph.D. in mathematics from the 
University of Chicago in 1997 under the direction of Saunders Mac Lane. 
In 2012-13, he was a member of the School of Mathematics at the 
Institute for Advanced Study, where he co-organized a special year 
devoted to Univalent Foundations of Mathematics along with V. Voevodsky 
and T. Coquand. Dr. Awodey is one of the inventors of Homotopy Type 
Theory and leads an active research group on that subject at Carnegie 
Mellon University, where he is a professor of philosophy and mathematics.

All are welcome! Coffee and cookies will be served in the Department 
Lounge (MS 461) after the presentation.