Samuel Mimram

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) and consists of 8 sessions of 3h. 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
  2. Identity types
  3. Homotopy levels
  4. Equivalences
  5. The fundamental group of the circle
  6. Higher inductive types
  7. Geometry
    • Higher homotopy groups
    • Deloopings of groups

Labs

We provide some cheat sheets for Agda and HoTT.

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

Exam

The exam is on paper with a pen. No documents are allowed excepting from this recto-verso page that you can edit here.

Books

Libraries

Latest news

People

If you are looking for internships, here is a (non-exhaustive) list of people working on topics related to this course:

Other