ESSLLI 2026
Introductory (Logic and Computation) course
10–14 August 2026
Homotopy type theory (HoTT), also known as univalent foundations (UF), offers a modern foundation for mathematics and an alternative to traditional set theory. A salient feature of HoTT is the fact that it has been implemented in computer proof assistants, notably Agda and Rocq, which are tools that can verify proofs encoded by a user. HoTT is an extension of Martin-Löf dependent type theory, but no familiarity with dependent type theory will be assumed. Instead, I will explain dependent type theory and the propositions-as-types interpretation to introduce and motivate univalent foundations. When it comes to HoTT, I will explain (1) its distinguishing features and techniques, like higher inductive types and the univalence axiom; (2) how to encode mathematics in it; and (3) illustrate the foregoing via examples in the Agda proof assistant.
Note: I had hoped to do some Agda in the lectures, but there isn't enough time. Come and talk to me if you'd like to learn Agda; we can set something up!
Note that lectures 2–5 will be blackboard/whiteboard lectures.
See resources.pdf and the slides for the first lecture for a brief discussion.
Your feedback on the lectures is most appreciated!
- Feedback form for Lecture 1
- Feedback form for Lecture 2
- Feedback form for Lecture 3
- Feedback form for Lecture 4
- Feedback form for Lecture 5 and whole course
I am grateful to the following people for their comments on the above slides.
- Jacob Neumann
- Linus Preusser
- Vojta Štěpaničik
- Pablo Rivas-Robledo