Schedule
Week 1 — Saturday, September 26 — Completed
Read PDTT Chapter 1: Introduction.
Covered a brief introduction to lambda calculus (α, β, and η rules), variable capture, the Y combinator and defining recursive functions with it, motivation for dependent type theory (types indexed by terms), the vector example, refl, and the difference between definitional and propositional equality.
Week 2 — Saturday, October 3
Read PDTT Section 2.1, “The simply-typed lambda calculus”; Section 2.2, “Towards the syntax of dependent type theory,” is optional.
Week 3 — Saturday, October 10
Read PDTT Section 2.2, “Towards the syntax of dependent type theory”; Section 2.3, “The calculus of substitutions”; and Section 2.4, “Internalizing judgmental structure: Π, Σ, Eq, Unit” (through 2.4.2).
Week 4 — Saturday, October 17
Read PDTT Section 2.4, “Internalizing judgmental structure: Π, Σ, Eq, Unit” (from 2.4.3), and Section 2.5, “Inductive types: Void, Bool, +, Nat.”
Week 5 — Saturday, October 24
Read PDTT Section 2.6, “Universes: U₀, U₁, U₂, …”
Week 6 — Saturday, October 31
Read PDTT Section 2.7, “Propositions and propositional truncation.”
Week 7 — Saturday, November 7
Read PDTT Section 3.1, “A judgmental reconstruction of proof assistants,” and Section 3.2, “Metatheory for type-checking.”
Week 8 — Saturday, November 14
Read PDTT Section 3.3, “A case study in elaboration: definitions,” and Section 3.4, “Models for metatheory.”
Week 9 — Saturday, November 21
Read PDTT Section 3.5, “The set model of type theory.”
Week 10 — Saturday, November 28
Read PDTT Section 3.6, “Equality in extensional type theory is undecidable” (a short reading), and review.
Week 11 — Saturday, December 5
Read PDTT Section 4.1, “Programming with propositional equality,” and Section 4.2, “Intensional identity types.”
Week 12 — Saturday, December 12
Read PDTT Section 4.3, “Limitations of the intensional identity type.”
Week 13 — Saturday, December 19
Read PDTT Section 4.4, “Observational type theory.”
Week 14 — Saturday, December 26
Optional paper reading session (winter break).
Week 15 — Saturday, January 2
Optional paper reading session (winter break).
Week 16 — Saturday, January 9
Optional paper reading session (winter break).
Week 17 — Saturday, January 16
Read PDTT Section 5.1, “Propositional univalence.”
Week 18 — Saturday, January 23
Read PDTT Section 5.2, “Homotopy type theory.”
Week 19 — Saturday, January 30
Read PDTT Section 5.2, “Homotopy type theory.”
Week 20 — Saturday, February 6
Read PDTT Section 5.3, “Cubical type theory.”
Week 21 — Saturday, February 13
Read PDTT Section 5.3, “Cubical type theory.”
Week 22 — Saturday, February 20
Read PDTT Section 5.4, “Computing with coercions and compositions.”
Week 23 — Saturday, February 27
Read PDTT Section 6.1, “Categories with families.”
Week 24 — Saturday, March 6
Read PDTT Section 6.2, “Pullback squares and Π, Σ, Eq, Unit,” and Section 6.3, “Orthogonality and Void, Bool, +, Nat” (through 6.3.4).
Week 25 — Saturday, March 13
Read PDTT Section 6.3, “Orthogonality and Void, Bool, +, Nat” (from 6.3.5), and Section 6.4, “Cwf morphisms and U₀, U₁, U₂, …”
Week 26 — Saturday, March 20
Read PDTT Section 6.5, “Democratic models and local cartesian closure.”
Week 27 — Saturday, March 27
Read PDTT Section 6.6, “Strictification constructions.”
Week 28 — Saturday, April 3
Read PDTT Section 6.7, “Canonicity via gluing.”