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.