Homotopy type theory is a formal system in which we can do mathematics. In this course, we will see how this works. In
particular, we will learn how a mathematical statement is expressed, what the difference between synthetic (a.k.a. axiomatic)
and analytic representation is, what univalence and higher inductive types are, and why truncation levels are important.
No prior familiarity of homotopy type theory is assumed, but basic knowledge of both type theory and category
theory will be helpful.
The main reference for this short course is the HoTT Book. I also recommend Egbert Rijke's book.
Exercises can be done on paper or in Agda. The Agda file contains some code that we discussed in the exercise session(s).
Exercises and
Agda and
whiteboard Thursday and
whiteboard Friday