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.
- Lecturer: Benno van den Berg
Room: ILLC, Science Park F2.43
ContentsThis 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.
FormatThe 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 detailsMeetings 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.
PrerequisitesKnowledge 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.
- 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.
To teaching page.