D.-C. Cisinski and Claudia Scheimbauer
Thursday 14-16, via zoom. Sign up on the mailing list.
Homotopy Type Theory is Martin Löf's dependent type theory together with Voevodsky's univalent axiom. This is a logic which aims at dealing with non-trivial identifications using abstract homotopy-theoretic methods. The aim of this seminar is to get aquainted with the basic theory: introduction of the axioms and of basic constructions and theorem related to classical homotopy theory.
We will mainly follow Egbert Rijke's lecture notes. We will also see Voevodsky's proof that a semantic interpretation of Homotopy Type Theory is the classical homotopy theory of Kan complexes, following the original paper of Chris Kapulkin and Peter LeFanu Lumsdaine.
Further references
for a nice overview:
M. Shulman, Homotopy type theory: the logic of space, to appear as a chapter of New Spaces in Mathematics, M.Anel and G.Catren(eds.), Cambridge University Press, 2021
for the precise link between syntax and semantic interpretation:
J. Cartmell, Generalised Algebraic Theories and Contextual Categories,
Annals of Pure and Applied Logic 32, 1986, 209-243
V. Voevodsky, A C-system defined by a universe category,
Theory and Applications of Categories, Vol. 30, 2015, No. 37, 1181-1214
Clive Newstead, Algebraic models of dependent type theory,
PhD thesis, Department of Mathematical Sciences, Carnegie Mellon University, 2018
for more on "Algebraic Topology as the new Peano Arithmetic":
The Univalent Foundations Program, Homotopy Type Theory:
Univalent Foundations of Mathematics(aka "The Hott Book"), Institute for Advanced Study, 2013
for implementation in AGDA or in Isabelle
| Date | Speaker | Topic |
|---|---|---|
| 12.11.20 | Kim Nguyen | Introduction (Notes) |
| 19.11.20 | Peter Hanukaev | Dependent function types and the natural numbers, Inductive types and the universe (Notes) |
| 26.11.20 | Tashi Walde | Identity Types, Equivalences (Notes) |
| 3.12.20 | Jakob Werner | Contractible types and contractible maps, the fundamental theorem of identity types |
| 10.12.20 | Niklas Kipp | The hierarchy of homotopical complexity, Function extensionality (Notes) |
| 17.12.20 | Benedikt Preis | Homotopy pullbacks, the univalence axiom (Notes) |
| 07.01.21 | Matteo Durante | The circle, Homotopy pushouts (Notes) |
| 28.01.21, 14:15 | Claudia Scheimbauer | Descent, sequential colimits |
| 28.01.21, 16:15 | Marco Volpe | The homotopy image of a map, set quotients |
| 04.02.21 | Tashi Walde | Homotopy groups of types, the long exact sequence of homotopy groups |
| 11.02.21 | Peter Hanukaev | The Simplicial Model of Univalent Foundations (after Voevodsky) |