2 Course calendar
We list the primary topics of each lecture on this calendar, for reference. If a topic isn’t finished in one lecture, it will be moved down the calendar.
If a topic is finished and there is remaining time, we will have time to work on homework, but will not speed up the class unless there is overwhelming consensus to do so.
Date | Topic |
Tue, Jan 10 | Propositional logic |
Thu, Jan 12 | Tactics |
Tue, Jan 17 | More tactics, Elaboration |
Thu, Jan 19 | Type theory |
Tue, Jan 24 | Normalization by evaluation |
Thu, Jan 26 | NbE questions |
Tue, Jan 31 | More NbE |
Thu, Feb 2 | Typed NbE |
Tue, Feb 7 | A2 questions, A3 questions |
Thu, Feb 9 | More A3, Π types |
Tue, Feb 14 | More Π, building Fin |
Thu, Feb 16 | Inductive types, recℕ |
Tue, Feb 21 | How to do A4 |
Thu, Feb 23 | Work on A4 |
Tue, Feb 28 | Σ types |
Thu, Mar 2 | Identity types, UIP, internalization |
Tue, Mar 7 | More identity types |
Thu, Mar 9 | Tarski universes |
Tue, Mar 21 | Part 2 logistics, introduction to Agda |
Thu, Mar 23 | A5 work session |
Tue, Mar 28 | HoTT: equivalences and bi-invertible maps |
Thu, Mar 30 | Agda: identity, Σ, universes |
Tue, Apr 4 | Agda: higher inductive types and Special Time™ |
Thu, Apr 6 | Agda: dependent eliminators for HITs (not present in class) |
Tue, Apr 11 | HoTT: contractibility |
Thu, Apr 13 | HoTT: propositions, sets, truncations |
Tue, Apr 18 | Agda: π₁(S¹) ≃ ℤ |
Thu, Apr 20 | HoTT: funext |
Tue, Apr 25 | HoTT: univalence (not present in class) |
Thu, Apr 27 | Agda: a little bit of cubical |