Homotopy Type Theory Seminar
Sommersemester 22
Veranstaltungsform: Presence and Online
Uni2Work-website of the seminar
https://uni2work.ifi.lmu.de/course/S22/MI/HoTT
This is the main website of the seminar.
Zeit und Ort
Fr 16-18; Beginn Mi 27. April 2022.
Link to the recurring zoom meeting
https://lmu-munich.zoom.us/j/95507842752?pwd=V0JzRWRUVmpxRzFYYkt5ZFZ5THJRQT09
Inhalt
The intuitionistic type theory of Martin-Loef, function-extensionality, the groupoid model of Hofmann and Streicher, Voevodsky?s axiom of univalence,
homotopy n-types, higher inductive types, the fundamental group of the higher circle, the Hopf fibration, the Freudenthal suspension theorem,
the van Kampen theorem, categories in HoTT.
Material
Presenations
- 24.04 I. Petrakis: Introductions and overview
- 04.05 M. Guerdi: Basic types of MLTT I
- 13.05 M. Guerdi: Basic types of MLTT II
- 20.05 L. Maio: The equality type I
- 27.05 L. Maio: The equality type II
- 03.06 L. Staudacher: The equality type and the other types of MLTT
- 10.06 M. Lorenz: Equivalences and the Function Extensionality Axiom
- 17.06 B. Blagojevic: The Univalence Axiom I
- 23.06 B. Blagojevic: The Univalence Axiom II
- 01.07 S. Woolfson: Higher Inductive Types I
- 08.07 S. Woolfson: Higher Inductive Types II
- 15.07 P. Vollmuth and M. Lauck: Category theory in HoTT
- 22.07 I. Andreou: Locally cartesian closed categories and type theory
- 29.07 L. Maio: Introduction to Cubical Type Theory
Letzte Änderung
24. Juli 2022
