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.
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.
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!
All lectures are recorded on video and can be watched in the HoTT-2019 video channel. The lecture notes are also available here.
There is a wealth of resources available on the topic of homotopy theory. The following literature is recommended as reading material:
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:
Egbert Rijke, Introduction to Homotopy Type Theory, a graduate course taught at Carnegie Mellon University. The accompanying lecture notes is recommended as reading material.
Martín Escardó, Introduction to Univalent Foundations of Mathematics with Agda is a set of lecture notes written in literal Agda (text interspersed with Agda code). It explains the basics very thoroughly and very well. You may safely ignore the fact that it is all formalized and computer-checked, altought you may also be interested in learning how to use Agda, in which case you can consult the lecture notes GitHub repository.
Here are some additional resources:
Z → Z × [0,1]Top with homotopy equivalences, Hurewicz fibrations, and Hurewicz cofibrationsX → Y where X is cofibrant and Y is fibrantTopHom(X,Y) with objects morphisms X → Y and morphisms equivalence classes
of left homotopies; interpretation in TopΠ, Σ0, 1, Nπ₁(S¹) = Zπ₁(S¹) = Z