Homotopy Type Theory

Introduction to 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.


Announcements; lecture notes and exercises

Creative Commons License Work by Ulrik Buchholtz licensed under a Creative Commons Attribution-Noncommercial-Share Alike 4.0 License.