22^nd Estonian Winter School in Computer Science (EWSCS)
XXII Eesti Arvutiteaduse Talvekool

Thorsten Altenkirch

School of Computer Science
University of Nottingham
United Kingdom

Introduction to homotopy type theory

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.

Course materials

• T. Altenkirch. Introduction to homotopy type theory. Notes for the EWSCS 2017 course. [pdf] (UPDATED!)


• Photos of whiteboards from the lectures.
• Lecture 1 [jpg]
• Lecture 2 [jpg]
• Lecture 3 [jpg]
• Lecture 4 [jpg]
• Videos from the lectures (unedited, large files).
• Lecture 1 [mts]
• Lecture 2 [mts]
• Lecture 3 [mts]
• Lecture 4 [mts]


• 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]

Last changed April 7, 2017 19:16 Europe/Helsinki (GMT +03:00) by local organizers, ewscs17(at)cs.ioc.ee
EWSCS'17 page: //cs.ioc.ee/ewscs/2017/