RequirementsStudents following this class are expected to have attended the introduction to programming and to formal proofs in Coq, or equivalent background.
Program requirementsExamen
TeacherHugo Herbelin
Weekly hours 4 h CM
Years

Syllabus

Basic Type Theory

  • Pure Type Systems
  • Martin-Löf's Type Theory
  • Calculus of Inductive Constructions
  • Proof/Program Correspondence
  • Proof Irrelevance
  • Inductive and Coinductive Types
  • Extensionality in Type Theory

Homotopy Type Theory

  • Type/Space and Equality/Path Correspondence
  • Homotopic Concepts in Type Theory (contractible spaces, h-levels, univalence, weak factorisation systems, fibrations, cofibrations)
  • Higher Inductive Types (spheres, quotients, truncations)
  • Axiom of Choice and Classical Reasoning In Homotopy Type Theory

Models

  • Categories with Families
  • Cubical Type Theory
  • Internal Translations
  • ω-groupoïdes
  • Kan complexes

Bibliography

  • THE UNIVALENT FOUNDATIONS PROGRAM : Homotopy type theory : Univalent foundations of mathematics (Institute for Advanced Study, 2013).