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.

**Lecture 1:**Type theory from a homotopy theory perspective (exercises)**Lecture 2:**Homotopy levels and equivalences (exercises [Agda file])**Lecture 3:**Univalent logic (exercises [Agda file])**Lecture 4:**Higher inductive types and synthetic homotopy theory

Last modified: Sun Aug 12 10:34:28 BST 2018.