Erik Palmgren: Voevodsky's foundations - type-theoretic background and the univalence axiom

This talk is the second in a series around Voevodsky's proposal for a novel foundations of mathematics based on notions from homotopy theory. We shall here present some background in Martin-Löf type theory, in particular pertaining to the identity types which are central to the approach, giving the notion of path. Furthermore the Univalence Axiom and its consequences are discussed. If time permits we also start presenting Voevodsky's standard model of type theory extended with this axiom.