University of Calgary
UofC Navigation

Awodey Explains Significance of Homotopy Type Theory to Philosophy of Mathematics

LogBlog Has Moved!

You are looking at the old blog archive. LogBlog has moved to
If you'd like to receive updates on new posts, please subscribe there!

Submitted by Richard Zach on Thu, 07/25/2013 - 12:12pm

Steve Awodey (CMU) explains the relevance of the foundational program of homotopy type theory and the univalence axiom to the philosophy of mathematics in a new preprint, "Structuralism, Invariance, and Univalence."

Recent advances in foundations of mathematics have led to some developments that are signicant for the philosophy of mathematics, particularly structuralism. Specically, the discovery of an interpretation of Martin-Löf's constructive type theory into abstract homotopy theory  suggests a new approach to the foundations of mathematics, with both intrinsic geometric content and a computational implementation. Leading homotopy theorist Vladimir Voevodsky has proposed an ambitious new program of foundations on this basis, including a new axiom with both geometric and logical signicance: 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 the framework of homotopical type theory.