Introduction to Homotopy Type Theory

Nicolai Kraus, at MGS 2021

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.

Annotated slides

Combined slides


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