Home

Awesome

Homotopy (type) theory

A doctoral course on homotopy theory and homotopy type theory given by Andrej Bauer and Jaka Smrekar at the Faculty of mathematics and Physics, University of Ljubljana, in the Spring of 2019.

In this course we first overview the basics of classical homotopy theory. Starting with the notion of locally trivial bundles, we motivate the classical definitions of fibrations, from which we proceed to identify the abstract strucure of Quillen model categories. We outline the basics of abstract homotopy theory in a Quillen model.

In the second part we introduce homotopy type theory from the point of view of classical homotopy theory, deliberately avoiding the connections between homotopy type theory and computer science. We show how type theory can be used to carry out homotopy-theoretic arguments abstractly and "synthetically". The fact that any construction expressed in type theory is homotopy invariant is both a blessing and a curse: a blessing because it never lets us step outside of the realm of homotopy theory, and a curse because we never step outside of the realm of homotopy theory.

Course administration

We meet weekly on Tuesdays from 14:00 to 16:00 in lecture room 3.06 at the Mathematics department.

The take-home exam is now available in exam.pdf.

Course materials

Homotopy theory

Anja Petković has kindly provided her course notes for the first part of the course, with the caveat that they very likely contain mistakes. Thank you, Anja!

Homotopy type theory

All lectures are recorded on video and can be watched in the HoTT-2019 video channel. The lecture notes are also available here.

External resources

Homotopy theory

There is a wealth of resources available on the topic of homotopy theory. The following literature is recommended as reading material:

Homotopy type theory

Being a new topic, homotopy type theory is still developing. Consequently, reading material and resources are a bit more fluid and scattered. A central resource is the "HoTT book", although it is hard-going for the unexperienced:

The following introductory notes are targeted at teaching homotopy type theory:

Here are some additional resources:

Course outline

Homotopy theory

Background & bundles

Background

Bundles

Fibrations of topological spaces, and their classification

Cofibrations & model structure

Homotopy and the homotopy category

Homotopies and suspensions in model categories

Homotopy type theory

Type theory (motivated by simplicial sets): Π, Σ

Video and notes.

Identity types as path objects

Video and notes.

Homotopy levels

Video and notes.

Equivalences

Video and notes.

Higher-inductive types

Video and notes.

Univalence and π₁(S¹) = Z

Video and notes.