Navigation

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.

Previous Edition

Registration

Via StudOn: https://www.studon.fau.de/crs3711899_join.html (to get a Zoom-link)

Running Plan of the Talks (TBA)

Date Speaker Title
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

HoTT and Cubical Type Theory

References on the Agda proof assistant

Other proof assistants