Prerequisites
Category theory or equivalent.

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
• Study how to formulate mathematics in type theory
• Understand how type theory with the univalence axiom is equivalence-invariant
• Study Voevodsky’s model of type theory in simplicial sets (“spaces”)
• Understand what the mathematical objects defined in (2) correspond to under the interpretation in simplicial sets

Lecturers
Paige Randall North, Utrecht University