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 ( 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


Via StudOn: (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 1)
19.05 TBA TBA
26.05 TBA TBA
2.06 TBA TBA
9.06 TBA TBA
16.06 TBA TBA
23.06 TBA TBA
30.06 TBA TBA
7.07 TBA TBA
14.07 TBA TBA

HoTT and Cubical Type Theory

References on the Agda proof assistant

Other proof assistants