Introduction to homotopy type theory
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.
- T. Altenkirch. Introduction to homotopy type theory. Notes for the EWSCS 2017 course. [pdf] (UPDATED!)
- Photos of whiteboards from the lectures.
- Videos from the lectures (unedited, large files).
- The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute of Advanced Study, 2013. [online version]
- The Cubical system. [sources]
- Agda. [language website, sources, instructions]
April 7, 2017 19:16 Europe/Helsinki (GMT +03:00)
local organizers, ewscs17(at)cs.ioc.ee
EWSCS'17 page: //cs.ioc.ee/ewscs/2017/