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:

• J. Davis & P. Kirk, Lecture Notes in Algebraic Topology (Chapter 4)
• R. Piccinini, Lectures on Homotopy Theory (Chapter 2)
• M. Hovey, Model categories (Chapters 1-3)
• A. Strom, The homotopy category is a homotopy category
• P. G. Goerss & J. F. Jardine, Simplicial homotopy theory (Chapters I and II)
• Daniel G. Quillen, Homotopical algebra

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:

• Univalent foundations program, Homotopy type theory: Univalent foundations of mathematics

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:

• Daniel Grayson: An introduction to univalent foundations for mathematicians, targeted at a general mathematical audience,
• Michael Shulman: Homotopy type theory: the logic of space, worth reading if you would like to expand your understanding of "space",
• Steve Awodey and Michael Warren: Homotopy theoretic models of identity types, the original paper introducing the interpreation of identity types in Quillen model categories.

Course outline

Homotopy theory

Background & bundles

Background

• What does (a part of) math deal with?
• Distinguishing between objects: relax, distinguish, stiffen
• Homotopy theory as a natural domain of algebraic invariants
• Homotopy theory as means of rephrasing a geometric problem

Bundles

• Bundles are omnipresent
• Vector bundle and its frame bundle
• Bundles with structure group
• Principal bundles and classification
• Lifting properties
• Homotopization of bundles

Fibrations of topological spaces, and their classification

• Hurewicz fibrations; definition in terms of the right lifting property with respect to inclusions Z → Z × [0,1]
• Pullbacks and retracts of fibrations are fibrations
• Any map decomposes functorially as a composite of a SDR inclusion followed by fibration
• The concept of a lifting function
• The fibres of a fibration are homotopy equivalent
• Homotopy fibre
• Puppe sequence

Cofibrations & model structure

• Homotopy extension property, cofibration, Eckmann-Hilton duality
• Pushouts and retracts of cofibrations are cofibrations
• Any map decomposes functorially as a composite of a cofibration followed by a fibration
• Quillen closed model category
• Model category on Top with homotopy equivalences, Hurewicz fibrations, and Hurewicz cofibrations

Homotopy and the homotopy category

• Cylinder object, left homotopy
• Path object, right homotopy
• Homotopy classes of maps X → Y where X is cofibrant and Y is fibrant
• Abstract localization and the homotopy category
• Cylinder object, path objects, and correspondence in the category of pointed topological spaces

Homotopies and suspensions in model categories

• Left homotopy of left homotopies in a model category, motivated by Top
• Correspondence between left and right homotopies
• The category Hom(X,Y) with objects morphisms X → Y and morphisms equivalence classes of left homotopies; interpretation in Top
• Suspension in a pointed model category and the suspension functor on its homotopy category

Homotopy type theory

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

Video and notes.

• Type theory as a theory of constructions
• The notion of a dependent type
• Types as sets, dependent types as families of sets
• Types as spaces, dependent types as fibrations
• Basic type-theoretic constructions:
  • dependent products
  • dependent sums
  • basic types 0, 1, N

Identity types as path objects

Video and notes.

• Identity types as path objects
• Type-theoretic rules for identity types
• Basic homotopy-theoretic constructions in terms of identity types:
  • the groupoid of paths
• Iterated identity types

Homotopy levels

Video and notes.

• Contractible spaces
• Propositions, sets, and h-levels
• Truncation as a type-theoretic construction
• The embedding of logic into type theory (using propositional truncation)
• Basic homotopy-theoretic constructions in terms of truncation:
  • loop space vs. fundamental group
  • path-connectedness vs. contractibility
  • surjectivity vs. split epimorphism

Equivalences

Video and notes.

• Structure vs. property in mathematics
• Having an inverse is not a property
• Homotopy equivalences
• Example: universal property stated as an equivalence

Higher-inductive types

Video and notes.

• Inductive types, examples
• Higher-inductive types (HITs)
• Examples: circle, interval, suspension
• Truncations as HITs

Univalence and π₁(S¹) = Z

Video and notes.

• The idea that equivalent structures are equal
• Univalence axiom
• Some consequences of the univalence axiom
• Example: π₁(S¹) = Z