Homotopy Type Theory

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.