Joint Seminar TUM/UR: Homotopy Type Theory

D.-C. Cisinski and C. 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
17.12.20 Benedikt Preis Homotopy pullbacks, the univalence axiom
07.01.21 Matteo Durante The circle, Homotopy pushouts
14.01.21 Descent, sequential colimits
21.01.21 The homotopy image of a map, set quotients
28.01.21 Tashi Walde Homotopy groups of types, the long exact sequence of homotopy groups
04.02.21 Peter Hanukaev The Simplicial Model of Univalent Foundations (after Voevodsky)
11.02.21 tba