Homotopy type theory is a formal system which serves as a programming language as well as a foundation of mathematics. It is a variation of Martin-Löf type theory, inspired by the observation that "types behave like spaces". Its novel features are Voevodsky's Univalence Principle (equivalence of types is equality of types) and higher inductive types (constructors for both elements and equalities).
This course will give a general introduction, demonstrate some of the exciting constructions, and discuss seemingly simple questions that are still open. The main reference will be the HoTT book.
Very rough notes and exercises:
lecture 1 (31st August 2019)
lecture 2 (2nd September 2019)
lecture 3 (3rd September 2019)