Lecturer: Bas Spitters
The online lectures will take place on Tuesday, April 13, 2021. All times are in UTC+2.
| Time | Topic |
|---|---|
| 14:00–14:45 | Part 1: Introduction to Coq and HoTT |
| 14:45-15:10 | Exercises |
| 15:10–15:30 | (break) |
| 15:30–16:15 | Part 2: h-Levels, type classes and HITs |
| 16:15–16:40 | Exercises |
| 16:40–17:00 | (break) |
| 17:00–17:45 | Part 3: Quotients and impredicativity, Axioms |
| 17:45–18:30 | Exercises |
We shall keep a strict schedule. Each block of two parts will consist of a lecture, followed by exercises and a discussion.
On the second day we shall dive deeper into HoTT and, in particular, its formalization in a proof assistant. We will use the Coq implementation of type theory, and specifically the HoTT library. There is much tutorial material available for Coq. Andrej Bauers's video tutorials are perhaps the most accessible. Software Foundations can also be useful.
Please make sure you have Coq with the HoTT library installed.
This second lecture series will partially follow the structure of the first lecture, but show how to formalize these aspects in HoTT.
Formalize the Exercises of day 1 using the HoTT library.
Optional exercises:
- Prove that the truncated logic from day1 (see part2.v) satisfies the (or some) rules of intuitionistic FOL.
- Advanced: Prove that the truncation HIT is equivalent to impredicative trunction. This uses resizing.
- Advanced: Prove the equivalence of quotients. This uses resizing.
There are also more advanced challenges in the text.
If you are a beginner, you will learn a lot by finding and replaying the existing lemmas. More experienced users are encouraged to write the statements and proofs from scratch.