Abstract

This series of talks is an introduction to Homotopy Type Theory and the Univalent Foundations of Mathematics. This new area of research develops a beautiful connection between algebraic topology (homotopy theory) and theoretical computer science (type theory).

The second talk will serve an introduction to the Univalent Foundations. This program started by Vladimir Voevodsky (IAS, Princeton) provides new interesting foundations of mathematics (based on type theory), naturally formalizing categorical and higher-categorical thinking. The main purpose of this project is to have a language based on homotopy types (as opposed to sets) that would enable one to easily prove results from homotopy theory using a proof assistant such as Coq. This can be accomplished by adding the Univalence Axiom to the standard set of rules of type theory. In the talk we will discuss the Univalence Axiom together with some of its basic consequences, higher inductive types, and a type theoretic proof of $\pi_1 (S^1) = \mathbb{Z}$.