EPIT 2020 - Spring School on Homotopy Type Theory course materials and planning.
Course units are organized into folders:
- Introduction to homotopy type theory
- The Coq-HoTT library
- Models of Homotopy Type Theory
- Cubical Type Theory and Cubical Agda
- Synthetic Homotopy Theory
We will also have two shorter lectures on:
- The Arend Proof Assistant by Valery Isaev
- Directed Homotopy Type Theory by Paige North
The program of the week will be lectures/exercise sessions from 2pm to 6.30pm (UTC+2). We will organize virtual social events in the evening.
Here is the day by day program, the detailed content and timing of each lecture can be found in the corresponding subfolder. YouTube channel: https://youtu.be/Ur_dMuEVppg
-
Day 1.
- Matthieu Sozeau and Nicolas Tabareau: Introduction
- Andrej Bauer: Introduction to Homotopy Type Theory
- Interleaved with exercise sessions
-
Day 2.
- Bas Spitters: The Coq-HoTT library
- Exercise session (with Discord)
- Prerequisite: check that you can run Coq with the HoTT library, following the instructions
-
Day 3.
- Christian Sattler : Models of Homotopy Type Theory
- Valery Isaev : Arend proof assistant
-
Day 4.
- Anders Mörtberg: Cubical Type Theory and Cubical Agda
- Exercise session (with Discord)
- Prerequisite: check that you can run Agda and build the agda/cubical library, following the instructions
-
Day 5.
- Egbert Rijke: Synthetic Homotopy Theory
- Paige North: Directed Homotopy Type Theory