PhD Course - Homotopy type theory seminar

Organizers:
Rasmus Møgelberg and Nicolas Pouillard

Lecturers:
None, this is a reading group

Date(s) of the course:
Starts 5th of February and will run in approximately 14 weeks every Wednesday 

Time:
10.00 – 12.00

Course description:
This seminar aims to bring together mathematicians and computer scientist interested in type theory, logic and the foundations of mathematics. We will study homotopy type theory starting at the most basic level, discussing both the type theory, the intuitions derived from homotopy theory and other models, and implementations in proof assistants. We will not assume previous knowledge of neither type theory nor homotopy theory.

The seminar will be based on online video lectures from a recent CMU course given by Bob Harper, as well as the HoTT book.

Program:
We meet once a week for two hours to discuss the main topics of the video and solve exercises. Each week we will assign one participant to summarise the video lecture and initialize the discussion. Exercises can be solved on paper or using a proof assistant (such as Coq or Agda). An introduction to the use of these tools will be provided. The seminar will run for approximately 14 weeks starting early February 2014.

Prerequisites:
Knowledge of either basic type theory, logic or category theory is a prerequisite. But we will start by covering basic type theory and not assume knowledge of homotopy theory.

Reading list:
The first 6-7 chapters of:
Homotopy Type Theory: Univalent Foundations of Mathematics. The Univalent Foundations Program. Institute for Advanced Study

Exam:
Active participation. Each student should take responsibility for initiating the discussion and summarizing the video lecture at one meeting.

Credits:
5 ECTS

Amount of hours the student is expected to use on the course:
Participation: 28 hrs.
Preparation : 112 hrs.

Website:
Can be found here