HOTT – Homotopy type theory

This is the webpage for the master 2 course Homotopy type theory (aka HOTT) taught at the Parisian Master of Research in Computer Science (MPRI).

Practical

The course takes place on Wednesdays in room 1004 of Sophie Germain building. It runs from December 10th, 2025 until February 25th, 2026, except December 24th and 31st (Winter holidays). The exam takes place on March 4th, 2026.

Course

The course roughly follows the HoTT book which can be considered as a textbook for this course. Reading Hatcher’s Algebraic Topology can also be a very good idea if you want to get more into the geometric side.

Slides

The slides for the courses can be found below:

1. Introduction
   • Introduction (handout)
   • Dependent types (handout)
   • Agda (handout)
2. Identity types
   • Identity types (handout)
   • Operations on identity types (handout)
3. Homotopy levels
   • Homotopy levels (handout)
4. Equivalences
5. The fundamental group of the circle
6. Higher inductive types
7. Geometry
8. Geometry

Labs

We provide some cheat sheets for Agda and HoTT.

1. Introduction to Agda
2. Identity types
3. Homotopy levels

Links

• the HoTT book
• Algebraic Topology by Allen Hatcher
• page of the course at MPRI