Thorsten Altenkirch

Abstract

Homotopy type theory is a new foundation of mathematics that generalizes Martin-Löf type theory to higher dimensions, that is non-trivial equality types. It introduces some new basic principles, such as the univalence axiom, which identifies isomorphic types. It also enables us to conduct an abstract version of homotopy theory which has exciting but largely unexplored applications to dependently typed programming. The course builds on the HoTT book, but will also cover some more recent developments like cubical type theory.

Thorsten's page for this course: http://www.cs.nott.ac.uk/~psztxa/ss-types-17/