Homotopy Type Theory SS17
Homotopy Type Theory (HoTT) is a new approach to foundations of logic, programming and mathematics. It has an increasingly powerful impact on the development of the modern type-theory based tools for programming and verification, such as Coq proof assistant and Agda programming language. The idea of the seminar is to provide a primer in HoTT and use the corresponding material to practice and improve research skills, such as being able to work with the literature, comprehend scientific texts, summarise and explain the material studied in front of an audience. We plan to use the material from the HoTT book (https://homotopytypetheory.org/book ) as a basis for the seminar. The actual topics will be discussed and distributed between students depending on their background and interests.
There is no formal registration process, but if you’re interested, you can send an email to Tadeusz Litak and Sergey Goncharov, just to help us estimate the number of participants (and possibly to have priority in the very unlikely case we’re overcrowded).
We’re scheduled for Mi, 14:15 – 15:45, Übung 3 / 01.252-128.
Slides
-
The first meeting: organizational slides with references and an easy introduction to constructive logic.
Martin-Löf lectures
Merlin has found a nicely re-typeset version.
Developments in other proof assistants
Something else I did not manage to show you: for comparison, here are developments in other proof assistants:
Running Plan of the Talks
| Date | Speaker | Title |
|---|---|---|
| Apr 26 | Tadeusz Litak | An easy introduction to constructive logic, [slides] |
| May 3 | Tadeusz Litak | Introductory chapters of the HoTT Book, till universes, [slides] |
| May 10 | Üsame Cengiz | Introductory chapters of the HoTT Book: dependent sums, products [slides] |
| May 17 | Tim Lukas Diezel | HoTT Book: Booleans, natural numbers, pattern matching and recursion [slides] |
| May 24 | Lukas Braun | HoTT Book: proposition types, identity types [slides] |
| May 31 | Jonathan Krebs | Basic concepts of Homotopy theory: Homeomorphisms, Homotopy equivalence, Fundamental group [slides] |
| Jun 7 | Jonathan Krebs | Basic concepts of Homotopy theory: Higher homotopy groups |
| Jun 14 | Michael Gebhard | HoTT Book: Types as higher grupoids, functions as functors, type families as fibrations |
| Jun 21 | Michael Gebhard | HoTT Book: Types as higher grupoids, functions as functors, type families as fibrations |
| Jun 28 | Paul Wild | HoTT Book: Homotopies and equivalences, higher grupoid structure of type formers [slides] |
| Jul 5 | Sergey Goncharov | Elementary Theory of the Category of Sets [slides] |
| Jul 12 | Lukas Braun | Ch. 2.9–2.11 [slides] |
| Jul 19 | Tim Lukas Diezel | Ch. 2.12, 2.13 [slides] |
| Jul 26 | Merlin Göttlinger | remainder of Chapter 2 [slides] |
Floating Slots
Those are the ones without a fixed time, and supposed to fill gaps in between the main talks.