Homotopy Type Theory

This course will cover some more advanced topics in homotopy type theory.

Prerequisites

I will assume some basic familiarity with basic Martin-Lof dependent type theory.

Resources

1. The Homotopy Type Theory Book
2. Introduction to Univalent Foundations of Mathematics with Agda
3. Introduction to Homotopy Type Theory

Exercises

I’ve started an hott-mgs repository for experimenting with HoTT in Agda. We can build out some of the basic structure during the exercise sessions. Feel free to clone and submit pull requests so that we make progress as the week progresses.

1. Exercise Sheet 1
2. Exercise Sheet 2
3. Exercise Sheet 3
4. Exercise Sheet 4

Course Topics

We will cover some of the basic concepts of homotopy type theory including:

1. h-Level
2. Equivalences
3. Univalence
4. Higher Inductive Types

Time permitting we will move on to more sophisticated topics like:

1. Homotopy Groups
2. Connectedness
3. Modalities