Homotopy type theory has been introduced at the beginning of the century, following the idea due to Voevodsky and collaborators that types (in the sense of type theory) should be interpreted as homotopy types (topological spaces considered up to deformation). This intuition can be made precise thanks to the univalence axiom, and a large body of work has now been developed. On the practical side, it provides the framework required in order to handle equality in type theory in full generality, as well as deal with associated coherence issues, thus motivating new developments in proof assistants such as Agda or Rocq. In particular, they suggested the introduction of higher inductive types which vastly generalize traditional inductive types, and motivated the introduction of “cubical” variants of type theory which behave nicely from a computational point of view. On the theoretical side, it enables one to reason about constructions in algebraic topology in a synthetic way, providing proofs which are correct and homotopy invariant by construction. This has allowed formalizing fundamental mathematical constructions (such as the computation of homotopy groups of spheres, or the cohomology of various spaces) and has suggested new proofs for some important theorems (such as the Blakers-Massey theorem) which hold in greater generality than previously known ones.

The objective of the course is to provide an introduction to homotopy type theory from the practical perspective given by proof assistants, with a view toward synthetic geometry. It will mainly focus on the logical foundations and the way of manipulating those in dependent type theory (there will be labs using the Agda proof assistant). Mathematical concepts should be introduced when needed.

Students are expected to master basic notions of logic, dependent types and proof assistants. We thus expcted that the courses PRFA (Proof assistants) and PRFSYS (Foundations of Proof Systems) were followed in the first period (or courses with similar contents such as the course CSC_51051_EP (Computational logic) at École polytechnique). The course SEMPL (Models of Programming Languages: Domains, Categories, Games) is also related to this one.

It can be useful (but this is not required) to have knowledge in category theory, topology (spaces, homotopy) and algebraic topology (fundamental groups, homology).

The course consists of 8 sessions of 3h: 2h of course followed by 1h of labs. The labs will consists in formalizing proofs in Agda.

Courses take place on Wednesday at 9h45 in room 1004 of Sophie Germain. First course is on December 10th 2025.

All the material for the course can be found on the dedicated webpage.

• Webpage for the course
• The HoTT book which serves as main reference for the course
• The Agda proof assistant
• Algebraic Topology by Allen Hatcher