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, from 8:45 to 11:45 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

Other

PhD thesis

Some interesting proposals for PhD thesis:

People

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