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

• Lecturer: Benno van den Berg
  Email: bennovdberg@gmail.com
  Room: ILLC, Science Park F2.43

Contents

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.

Format

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.

Prerequisites

Knowledge of type theory is not essential, although obviously useful. Here are some recommended texts on type theory:

• Per Martin-Löf. Intuitionistic type theory. Bibliopolis, 1984. Available here.
• Bengt Nordström, Kent Petersson and Jan M. Smith. Martin-Löf's Type Theory. Chapter from the Handbook of Logic in Computer Science, Volume 5, Oxford University Press, 2000. Available here.
• Bengt Nordström, Kent Petersson and Jan M. Smith. Programming in Martin-Löf's Type Theory. Oxford University Press, 1990. Available here.

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.