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 typetheory 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.252128.
Slides

The first meeting: organizational slides with references and an easy introduction to constructive logic.
MartinLöf lectures
Merlin has found a nicely retypeset 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.