Introduction to homotopy type theory
- Pierre-Louis Curien. CNRS, Université de Paris, INRIA, Francia.
- Track de Fundamentos de Lenguajes de Programación.
Nota: El curso será dictado en Inglés
In this course, we shall introduce the basic concepts of Martin-Löf’s type theory: dependent types, sigma types, pi types, inductive types, identity types. We shall then proceed to describe its recent extension called homotopy type theory (HoTT), after ideas of Voevodsky: univalence axiom, higher inductive types. Finally, we shall give applications of HoTT in the development of mathematical proofs, focusing on synthetic homotopy theory.
The course will be based on the HoTT book, freely available from https://homotopytypetheory.org/book/ as well as on some recent research articles on synthetic homotopy theory, such as Guillaume Brunerie’s paper (available from https://guillaumebrunerie.github.io): The James construction and pi4(S3) in homotopy type theory, Journal of Automated Reasoning 63(2).
• Introduction to type theory • Dependent types, sigma types, pi types, inductive types, identity types • Univalence axiom, higher inductive types • homotopy groups.
Students ideally would have some basic knowledge of functional programming (ML or Haskell), and would have some mathematical background/mind (proofs by induction, in particular, ability to conduct structured reasoning). Some basic knowledge in topology will help. But none of these skills will be actually required, as the course will be as self-contained and slow-pace as possible.