A survey of Univalent Foundations (by Eric Finster, November 13th, 2014)

We give an overview of the foundational point of view advocated by Voevodsky’s Univalent Foundations program and explain how these ideas are realized by Martin-Lof type theory with identity types. In particular, we focus on the role of the univalence axiom as an invariance principle, embedded in type theory, which is absent from traditional set-theoretic foundations, and explain how this point of view leads to a unification of certain logical and geometric principles.