Homotopy Type Theory - M2 - 8EC

 

Prerequisites

 

Familiarity with basic concepts of category theory will be assumed: limits and colimits, adjoint functors, monads, presheaves, and the Yoneda Lemma. The Mastermath Category Theory course is sufficient, or knowledge of Chapters I-VI of Mac Lane's Categories for the Working Mathematician (2nd edition).

 

Aim of the course

 

Type theory was introduced in the 1970’s as a foundation of mathematics expressed in a functional programming language. It has become a powerful tool in the computer verification of mathematical proofs and correctness of software. Recently, a homotopy-theoretic interpretation of type theory has been developed, yielding an intuition of types as spaces, that is, as geometric objects which are typically studied in the mathematical field of homotopy theory. This gave rise to the program of homotopy type theory.

 

Via Voevodsky’s univalence axiom, which is inspired and validated by the homotopy-theoretic interpretation, type theory becomes invariant under equivalence of structures - this is the univalence principle.

 

The aims of the course are to:

 

- Introduce type theory both as a mathematical formalism and one implementation of it as a programming language

- Study how to formulate mathematics in type theory (both in the mathematical formalism and in the programming language)

- Understand how type theory with the univalence axiom is equivalence-invariant

- Study the categorical semantics of type theory

- Study Voevodsky’s model of type theory in simplicial sets (“spaces”)

Rules about Homework/Exam
 
There will be homework assignments during the course, the average of which counts for 40% of the final grade. The course will be concluded by a final exam which has two components: a take-home part and an oral part. This final exam counts for the remaining 60% of the grade, and you must obtain a grade of at least 5 in the final exam. (This applies to the retake exam as well.) You must hand in each homework assignment to take the final exam (or retake).
 
Lecture Notes/Literature
 
The following textbooks are relevant to the course. Relevant papers will be suggested during the course.
 
- Homotopy Type Theory. Available from https://homotopytypetheory.org/book/.
- Introduction to Homotopy Type Theory by Egbert Rijke. Available fromhttps://arxiv.org/abs/2212.11082.
 
Lecturers
 
Paige Randall North, Utrecht University