Homotopy Type Theory 2015

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 2015.
A list of possible presentation topic can be found here.
Participants of this student seminar may be interested in attending the Utrecht Workshop on Proof Theory, April 16-18, where Per Martin-Löf is one of the invited speakers. See here.

Teaching staff

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, for which they will prepare a handout.

Practical details

Meetings are on Wednesday from 15:00-17:00 in SP G3.02 and Fridays from 13:00-15:00 in SP G0.05, starting from Wednesday 1 April till Friday 22 May.

The following is the schedule for the meetings from week 16 onwards:
Week 16 15 April: Final Lecture
17 April: No lecture, lecturer at conference
Week 17 No lectures or presentations: meetings with the lecturer to discuss presentations
Week 18 29 April: Evan and Thomas on Chapter 3 of the HoTT book
1 May: Auke and Daniil on categorical models of type theory, see papers by Hofmann and Pitts
Week 19 6 May: Jeroen and Sander on Chapter 4 of the HoTT book
8 May: Bobby and Nils on the groupoid model, see Hofmann and Streicher, The groupoid interpretation of type theory. Available here
Week 20 No presentations (lecturer has other obligations on 13 May and 15 May is a holiday)
Week 21 20 May: Anna and Joost on Chapter 9 of the HoTT book
22 May: Guillaume and Mees on Voevodsky's model in simplicial sets, see here

Prerequisites

Knowledge of type theory is not essential, although obviously useful. 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.