Homotopy Type Theory is a new foundation of Mathematics which generalizes Martin-Löf Type Theory to higher dimensions, that is non-trivial equality types. It introduces some new basic principles, such as the univalence axiom, which identifies isomorphic types. It also enables us to conduct an abstract version of homotopy theory which has exciting but largely unexplored applications to dependently typed programming. This course will give a taster of the material in the book Homotopy Type Theory: Univalent Foundations of Mathematics which is the outcome of a special year at the Institute of Advanced Studies in Princeton, which I attended. The book is available for free from the internet in electronic form but you can also obtain a printed version at a low price.