Homotopy Type Theory SS21
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 and Agda proof assistants/certified programming environments. The idea of the seminar is to provide a primer in HoTT and related extensions of Martin-Löf Type Theory (MLTT) such as Cubical Type Theory (more computational in nature than HoTT) and use the corresponding material to practice and improve research skills, such as being able to work with the literature, comprehend scientific texts, summarize and explain the material studied in front of an audience.
We regard the HoTT book (https://homotopytypetheory.org/book) as a unifying background reference, but plan to propose as bases for the actual presentations, tutorials and accessible research articles — see below for a tentative list of sources.
Moreover, we intend to involve proof assistants, based on dependent type theories to practice and illustrate main ideas and principles. The topics will be discussed and distributed between students depending on their background and interests. We expect a certain degree of flexibility in presentation formats, including at least talks with prepared slides and tool demonstration sessions.
We’re scheduled for Mi, 14:15 – 15:45 (online, due to the COVID19 restrictions). First meeting: 14.04, check out StudOn, for the Zoom-link.
Via StudOn: https://www.studon.fau.de/crs3711899_join.html (to get a Zoom-link)
Running Plan of the Talks (TBA)
|21.04||Sergey Goncharov||Introduction to Martin-Löf type theory (Part 1)|
|28.04||Sergey Goncharov||Introduction to Martin-Löf type theory (Part 2)|
|5.05||Aaron Strahlberger||Spartan Agda (Part 1)|
|12.05||Aaron Strahlberger||Spartan Agda (Part 2)|
|19.05||Alexander Trzeciak||An introduction to univalent foundations for mathematicians (Part I)|
|26.05||Alexander Trzeciak||An introduction to univalent foundations for mathematicians (Part II)|
|2.06||Stefan Licklederer||What is homotopic about the homotopy type theory?|
|9.06||David Wegmann||Formalizations in Spartan Agda, singletons and subsingletons (Part I)|
|16.06||David Wegmann||Formalizations in Spartan Agda, singletons and subsingletons (Part II)|
|23.06||Alexander Trzeciak||An introduction to univalent foundations for mathematicians (Part III)|
|30.06||Nicolas Wachsmann||Voevodsky’s notion of equivalence and the univalence axiom in Agda (Part I)|
|7.07||Nicolas Wachsmann||Voevodsky’s notion of equivalence and the univalence axiom in Agda (Part II)|
|14.07||Sergey Goncharov||A brief introduction to Cubical Agda|
General type theory (MLTT and its extensions)
HoTT and Cubical Type Theory
- Daniel R. Grayson, An introduction to univalent foundations for mathematicians
- A course on homotopy (type) theory by Andrej Bauer and Jaka Smrekar
- Steve Awodey, Type theory and homotopy
- Bruno Bentzen, Naive cubical type theory
- Anders Mörtberg, Cubical methods in homotopy type theory and univalent foundations
References on the Agda proof assistant
- Martín Escardó, Agda in a hurry
- Martín Escardó, A brief Agda tutorial
- Philip Wadler,Wen Kokke, Jeremy G. Siek, Programming Language Foundations in Agda
- Martín Escardó, Introduction to Univalent Foundations of Mathematics with Agda