Carnegie Mellon University
file.pdf (211.31 kB)
Download file

Structuralism, Invariance, and Univalence

Download (211.31 kB)
journal contribution
posted on 2013-03-04, 00:00 authored by Steven AwodeySteven Awodey

The recent discovery of an interpretation of constructive type theory into abstract homotopy theory suggests a new approach to the foundations of mathematics with intrinsic geometric content and a computational implementation. Voevodsky has proposed such a program, including a new axiom 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. It also gives the new system of foundations a distinctly structural character.


Publisher Statement

Copyright The Author [2013]. Published by Oxford University Press. The version of record is available online at



Usage metrics