The usual foundations of mathematics based on Set theory and
Predicate calculus (and extended by category theory), while successful in many
ways, are so far removed from everyday mathematics that the possibility of
translation of theorems to their formal counterparts is generally purely a
matter of faith. Homotopy type theory gives alternative foundations for
mathematics. These are based on an extension of type theory (from logic and
computer science) using an unexpectedly deep connection of Types with Spaces
discovered by Voevodsky and Awodey-Warren. As a consequence of this relation we
also obtain a synthetic view of homotopy theory.
In this lecture, I will give a brief introduction to this young subject.