Homotopy Type Theory 2017

This is the website for the student seminar on ``Homotopy Type Theory'' which will be offered at the University of Amsterdam in September and October of 2017.
A list of possible presentation topics can be found 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.

Every student gives one blackboard (seminar-style) talk. One is also required to make a handout for the other students. Students work in pairs; each session there will be two presentations of 45 minutes (but in each presentation, leave 5 minutes for discussion).

Additionally, every pair of students formulates a homework exercise, which the other participants do, and hand in to the speaker a week later. The speaker then grades this work and hands everything (including a model solution) to the teacher. The teacher, after examination, hands the grades to the participants. Make also a grading scheme: if an exercise consists of more than one part, tell the students what each part is worth.

Attendance at the presentations by the other students is compulsory.

Grade

Your final grade is composed of your grade for the presentation (40%, of which 20% for understanding the mathematics and 20% for communicating it), the handout (10%), the formulation and grading of the homework exercise (10%) and your solutions to the other speakers' exercises (40%).

Practical details

Meetings are on Wednesdays from 11:00-13:00 in F2.19 in SP 107 and Fridays from 11:00-13:00 in F2.19 in SP 107, starting from Wednesday 5 September till Friday 20 October.

The schedule for the presentations is as follows:
Date Presenters Topic Handout
4 October Matteo and Sam Chapter 3 from the HoTT book here
6 October Daniel and Tim Chapter 4 from the HoTT book here
11 October Jan and Robert Hofmann on the semantics of type theory here
13 October Ethan and Max The groupoid model of type theory here
18 October Krsto and Marlou Type theory and weak factorisation systems (Awodey-Warren, Gambino-Garner) here

Prerequisites

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.