RequirementsBasic knowledge in category theory
Program requirementsCC+examen
TeacherPierre-Louis Curien
Weekly hours 2 h CM
Years Master Logique et Fondements de l'Informatique


Homotopy theory, which is devoted to the study of spaces up to deformation, has given rise to a branch of algebra called homotopical algebra, in which tools are developed for dealing with structures in which laws like associativity do not hold exactly like in classical algebra, but up to homotopy, these homotopies being themselves subject to coherences, etc.

Homotopy theory has also a logical side, in which types, proofs of equality, and proofs of equality of proofs of equality are interpreted as spaces, paths, and homotopies between paths, respectively. The notion of fibration, that plays an essential rôle in homotopy theory, is tightly related with substitution in dependent type theory. This interplay has led to a new version of type theory called homotopy type theory.

The course is a follow-up of that on category theory taught in the first semester, but can be followed by students who have already some basic background in category theory. We shall introduce the important notions underlying the subject: enriched categories, model categories, as well as different approaches to the definition of higher catégories, notably via simplicial sets. We shall also hint at connected subjects such as operads and ∞-operads, that also have arisen from topology. The lectures will partly follow the flow of exposition found in recent books (Categorical homotopy theory by Emily Riehl, The homotopy theory of (∞, 1)-categories by Julia Bergner, From categories to homotopy theory by Birgit Richter, Higher categories and homotopical algebra by Denis-Charles Cisinski, Simplicial methods for higher categories by Simona Paoli, which all offer opportunities to the interested students for learning more), with an eye on the links with homotopy type theory.