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.



Tue, Jan 10

Propositional logic

Thu, Jan 12


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