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.
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
|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)|