1) Prerequisites
Category theory or equivalent.
2) 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”)
3) 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 an exam, for which you must obtain a grade of at least 5, and which counts for 60% of the final grade. (This applies to the retake exam as well.) You must hand in each homework assignment to take the final exam (or retake). The exact format of the final exam will be announced closer to the time.
4) 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.
- Introduction to Homotopy Type Theory by Egbert Rijke. Available from https://arxiv.org/abs/2212.
- Docent: Paige North