Lecture 1: Type Theory (by Paige Randall North)
Lecture 2: Type Theory (by Niels van der Weide)
Lecture 3: Univalent Foundations (by Paige Randall North)
Lecture 4: Tactics in Coq (by Benedikt Ahrens)
Lecture 5: Set-Level Mathematics (by Carlo Angiuli)
Lecture 6: Univalent Category Theory (by Niels van der Weide)
Lecture 7: Synthetic Homotopy Theory (by Favonia)
Lecture 1: Type Theory (by Gianluca Amato)
Lecture 2: Fundamentals of Coq (by Marco Maggesi)
Lecture 3: Univalent foundations (by Paige Randall North)
Lecture 4: Tactics in UniMath (by Ralph Matthes)
- Lecture (HTML for easier reading)
- Lecture (Coq file presented in class)
- Extended Lecture (HTML)
- Extended Lecture (Coq file)
- Exercises
- Advanced exercises
- Solutions
- Advanced solutions
Lecture 5: Set-Level Mathematics (by Benedikt Ahrens)
Lecture 6: Univalent Category Theory (by Niels van der Weide)
Lecture 7: Synthetic Homotopy Theory (by Peter LeFanu Lumsdaine)
Lecture 1: Spartan Type Theory by Andrej Bauer
Lecture 2: Fundamentals of Coq by Anders Mörtberg
Lecture 3: Univalent Foundations by Martín Hötzel Escardó
Lecture 4: Tactics by Ralph Matthes
- Lecture (short version)
- Lecture (long version)
- Exercises
- Advanced exercises
- Solutions
- Advanced solutions