The new subject of "homotopy type theory" has been created by a fusion of homotopy theory, higher category theory, and constructive type theory. On one hand, it enables us to apply homotopical ideas in type theory, giving new ways to deal with things like proof-irrelevance, singleton elimination, type equivalence, and universes. On the other hand, it gives us a formal language in which to do homotopy theory. A proof written in this language will automatically be valid in many different ``homotopy theories", and can also be formalized and checked by a computer proof assistant. Taken to an extreme, the subject offers the possibility of a new foundation for mathematics in which the basic objects are homotopy types, rather than sets. This is the beginning of a weekly seminar which will introduce the subject and some of its highlights, assuming no background in either homotopy theory or type theory. In addition to the mathematical theory, we will learn to formalize it using the computer proof assistant Coq.