Homotopy Type Theory 2016

This is the website for the student seminar on ``Homotopy Type Theory'' which will be offered at the University of Amsterdam in April and May of 2016.

A list of possible presentation topics can be found here.

Teaching staff


This course will be devoted to type theory, in particular some recent developments in connecting the topic to homotopy theory. Type theory dates back to the work of Russell from the 1920s, but in the hands of Per Martin-Löf it became a foundational system for constructive mathematics. But at the same time, type theory can also be seen as a programming language and lies at the basis of proof assistants, such as Agda and Coq. Homotopy type theory refers to some recent work aiming to further understand and extend type theory by introducing concepts from category and homotopy theory (algebraic topology). New concepts which have appeared include higher inductives types and Voevodsky's univalence axiom; also, they lead to a new ("synthetic") way of doing homotopy theory. The idea of the course is be flexible as regards as to its precise contents. We will at least look at categorical models, but we will also look at more syntactic developments. But the precise contents will depend on the interests of the participants.


The format of the course will be that of a student seminar, in which the lecturer will give some lectures, but most of the course will consist of presentations given by students.

Practical details

Meetings are on Tuesdays from 9:00-11:00 in SP D1.162 and Fridays from 9:00-11:00 in SP G2.13, starting from Tuesday 29 March till Friday 20 May.

Week 13 29 March: Lecture
1 April: Lecture
Week 14 5 April: Lecture
8 April: Lecture
Week 15 No lectures or presentations: meetings with the lecturer to discuss presentations
Week 16 19 April: Sven and Tom on identity types and weak factorisation systems: Gambino and Garner, Awodey and Warren
22 April: Workshop on the occasion of the retirement of Albert Visser, see here
Week 17 26 April: Stella and Anton on Chapter 3 of the HoTT book
29 April: Bas and Menno on Chapter 4 of the HoTT book
Week 18 3 May: Sven and Tom on Chapter 9 of the HoTT book
6 May: Holiday (day after Ascension Day)
Week 19 10 May: Stella and Anton on the univalent model in simplicial sets, see here
13 May: Bas and Menno on types as omega-groupoids: Van den Berg and Garner, Bourke and Lumsdaine
Week 20 18 May, 11:00-13:00 in D1.160. Presentations by Nils Donselaar and Daniil Frumin.


Knowledge of type theory is not essential, although obviously useful. Here are some recommended texts on type theory: What will be more than useful is a knowledge of basic category theory, say at the level of Steve Awodey's book Category Theory, Oxford Logic Guides 52, OUP, 2010.

To teaching page.