Meeting time and place: Tue/Thu 12:00 - 1:20, Baker Hall 150

Instructor: Egbert Rijke (erijke[at]andrew.cmu.edu)

Office: Baker Hall 148

Office Hours: Mon/Wed 5:00 - 6:00, or by appointment

Full notes (in progress, last modified: )

HoTT book: sections 6.2, 6.5, 6.7, 6.8

*An overview of all the lectures with links to the previous notes and exercises is given below.*

Homotopy Type Theory (HoTT) is a new field of mathematics that extends Martin-Löf's dependent type theory by the addition of the univalence axiom and higher inductive types. In HoTT we think of types as spaces, dependent types as fibrations, and of the identity types as path spaces. We will see that many spaces that are familiar to topologists can be represented as higher inductive types, and we will develop the basic theorems and constructions in HoTT to reason about them.

We will roughly follow the book Homotopy Type Theory: Univalent foundation of mathematics, of which a PDF is freely available.

Some of the later results of synthetic homotopy theory can only be found in recent research papers. We will also use the PhD thesis of Guillaume Brunerie as a resource.

Each session will consist of two parts: a 50 minute lecture and 30 minutes in which students present solutions to exercises provided with the previous lecture. These presentations are intended to be short (roughly 5 minutes) and focused to the problem at hand. Problem sets will be posted below with the lecture synopses.

Students are expected to:

- Present a solution when they are asked to do so (usually a week in advance). Graduate students will be asked to present more often than undergraduate students.
- Per lecture, either correct a somewhat substantial mistake in the notes and exercises, or hand in a written solution for one exercise of their choice. Written solutions are to be handed in at the start of the next lecture for an A, or at the start of the next lecture after that for a B. Collaborations are encouraged, but solutions must be handed in individually. Presenting students hand in a written solution for the exercise they are asked to present.

Hints for the exercises will be presented by the instructor during office hours, a day before they have to be handed in.

Note: The lectures are still in preparation, and in particular the topics of the lectures after the spring break may be subject to change.

HoTT book: The introduction, and section 1.1

HoTT book: sections 1.2, 1.4, 1.9

HoTT book: sections 1.3, 1.5, 1.6, 1.7, 1.8

HoTT book: sections 1.11, 1.12, 2.1, 2.2

HoTT book: sections 2.4, 2.7

HoTT book: sections 3.11, 4.4

HoTT book: sections 4.7, 2.12, 8.9. Look for the `encode-decode method'.

HoTT book: sections 3.1, 3.3, 7.1, 7.2

HoTT book: sections 2.9, 2.15

HoTT book: does not have an introduction to pullbacks.

HoTT book: 2.10, 4.8, 9.8, 10.1

HoTT book: sections 6.1, 6.2, 6.4

HoTT book: sections 6.2, 6.5, 6.7, 6.8

- Location: 427 Thackeray Hall
- Time: 12:00pm