Philip Hackney, firstname.lastname@example.org
Peter LeFanu Lumsdaine, email@example.com
The first half of the course will be a brief introduction to (∞,1)-categories, which are becoming an increasingly important tool in homotopy theory, derived algebraic geometry, topological quantum field theories, type theory, etc. Particular emphasis will be placed on quasi-categories, which are certain simplicial sets which look like the nerve of a category except that iterated compositions are only weakly defined. We will discuss the Joyal model structure on the category of simplicial sets (for which the cofibrant-fibrant objects are precisely the quasi-categories) and see how to translate many categorical concepts to this setting. We will also examine other models for (∞,1)-categories, such as simplicial categories and Rezk's complete Segal spaces. Finally, we will try to give an idea about how (∞,1)-categories are a natural home for abstract homotopy theory.
The second part of the course will give an introduction to Homotopy Type Theory (HoTT), exploring recently discovered connections between type theory (from mathematical logic) and homotopy theory.
The main focus will be Voevodsky's model in simplicial sets. Specifically, this uses Kan complexes (a subclass of quasi-categories, and probably the best-studied model of ∞-groupoids) to model Martin-Löf dependent type theory, a logical system widely used as a basis of formal proof systems such as Coq and Agda. Moreover, this model possesses two powerful extra features: higher inductive types and univalent universes, constructs corresponding roughly (in the language of (∞,1)-categories) to homotopy colimits and an object classifier. These allow one to develop homotopy theory axiomatically within the type theory, and to view it as a foundation for mathematics based not just on discrete sets, but on spaces in the homotopy-theoretic sense.
No previous knowledge of type theory or mathematical logic will be assumed.
André Joyal, The Theory of Quasi-categories and its Applications
Various authors, Homotopy Type Theory: Univalent Foundations of Mathematics
Nordström–Petersson–Smith, Programming in Martin-Löf’s Type Theory
In class on November 18 Philip mentioned the model structure on Cat. Charles Rezk has a short proof of the existence of this model structure, http://www.math.uiuc.edu/~rezk/cat-ho.dvi. As for uniqueness, see this blog post and this mo comment.