Abstract:

Homotopy type theory is a variation on Martin-Löf type theory with new features inspired by models based on abstract homotopy theory. These include Voevodsky's Univalence Axiom, which identifies equivalent types, and higher inductive types, which makes it possible to construct new freely generated types with non-trivial identity types. This course will give an introduction to these concepts, and show how they can be used for so-called synthetic homotopy theory, but also for ordinary mathematics and dependently typed programming. We will build on the HoTT book, but also refer to more recent developments such as the computational interpretation of homotopy type theory in cubical type theory.

The course material is available at https://personal.cis.strath.ac.uk/fredrik.nordvall-forsberg/ohrid-school-hott2018/.