2nd Semester 2013/14: Homotopy Type Theory
- Instructors
- ECTS
- 6
- Description
- Homotopy type theory refers to new developments around constructive type theory, shedding light one of its more mysterious aspects: its treatment of equality. Originally, type theory was invented to give precise expression to Per Martin-Löf's constructivist convictions; but he also pointed out that his type theory could be regarded as a functional programming language. As such it lies at the basis of proof assistants like Agda and Coq, in which one can formally verify one's mathematical proofs.
Several treatments of equality exist, but the one preferred by Martin-Löf and with the nicest computational behaviour, is also the most mysterious. Recently it has become clear that ideas from homotopy theory makes this "intensional" treatment of equality quite natural. This reading also suggests several extensions of type theory, such as Voevodsky's univalence axiom and higher inductive types, which allow one to recapture extensional properties of type theory.
Homotopy type theory can also be seen as a structuralist foundations of mathematics, incorporating features incompatible with usual foundational schemes. Types are defined purely in terms of their structural (categorical) properties and this is exploited by the univalence axiom, which roughly says that isomorphic types are equal.
The idea of the course is that students give presentations about topics of their choice in homotopy type theory. We will certainly want to have a look at categorical models of type theory, as they provide the best way of understanding the main ideas. Besides more technical work, it is also possible to explore the topic's more philosophical aspects (constructivism, structuralism).
- Organisation
- There will be around three introductory lectures, after which the participants will give presentations on a topic of their choice.
- Prerequisites
- Basic category theory. Some notion of type theory would be helpful, but is not required. Knowledge of homotopy theory is certainly not required.
- Assessment
- This is a 6 EC project. Students will be asked to demonstrate understanding of the course materials through a written report and an oral presentation. Participation in the group discussions will also contribute to the assessment.
- References