- Home
- Arbeitsgruppe / Team
- Lehre / Teaching
- Forschung / Research
- Curriculum Vitæ
- Fakultät für Mathematik
- SFB 1085 Higher Invariants

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 |