TITLE: Homotopy type theory and univalent foundations

ABSTRACT: This talk will introduce alternative foundations for mathematics in which “equality” becomes “identity,” which is no longer a mere predicate but can carry structure. The primitive notion is called a “type,” which can be interpreted as something like a set, or as something like a mathematical proposition, as a something like a groupoid or moduli space, which has higher structure. What Voevodsky named the “univalent foundations of mathematics” arose from a recently discovered homotopy theoretic interpretation of dependent type theory, originally designed as a formal system for constructive mathematics. We will introduce this formal system, explore Voevodsky’s univalence axiom and its consequences, and discuss advantages for computer formalization.