Homotopy Type Theory

Information about the course

Part I will be a gentle introduction to type theory and constructive mathematics for (mathematics and computer science) students with no previous exposure to either. We shall introduce the constructions of type theory with the homotopical interpretation in mind, and build up enough results to do a bit of synthetic homotopy theory, leaving the participants able to go further on their own.

Administrative matters

• Lectures: Mondays 13:30–15:10 in S102/144, Tuesdays 15:20–17:00 in S215/409K (Half of the Tuesday lecture is for group discussions of the exercises; sometimes the other half will be demonstrations of proof assistants for type theory/HoTT.)
• Office hours: Thursdays 13:30–15:10 in S215/230, or by appointment.
• Prerequisites: none (some mathematical maturity and curiosity). Optional (but helpful): topology, algebraic topology, algebraic geometry, category theory, and/or functional programming.
• Zulip chat group.

References

• Egbert Rijke: Introduction to Homotopy Type Theory (pdf)
• Andrej Bauer: Homotopy (type) theory Course
• Univalent Foundations Program: The HoTT Book
• Martín Hötzel Escardó: Introduction to Univalent Foundations of Mathematics with Agda
• Simon Thompson: Type Theory & Functional Programming
• Avigad–de Moura–Kong: Theorem Proving in Lean
• Kevin Buzzard and Mohammad Pedramfar: The Natural Number Game

Announcements; lecture notes and exercises

• Lecture 1 (October 14), addendum (October 15)
• Lecture 2 (October 21), addendum (October 22)
• Office hours are cancelled on October 24
• Lecture 3 (October 28)
• Lecture 4 (November 4)
• Lecture 5 (November 11)
• Lecture 6 (November 18)
• Lecture 7 (November 25)
• Lecture 8 (December 2), addendum (December 3)
• Lecture 9 (December 9)
• Lecture 10 (December 16)
• The class on December 17 is cancelled: You are encouraged to join the algebra seminar, where Johan M. Commelin will talk about formalizing perfectoid spaces. It's 15:00–16:15 in S215-401.
• Lecture 11 (January 13)
• Lecture 12 (January 20)
• Lecture 13 (January 27)
• Lecture 14 (February 3)
• Lecture 15 (February 10)