slideshow 3

Logic seminar

Introduction to homotopy type theory

Valery Isaev
JetBrains research


Monday, 24. May 2021 - 15:45 to 17:15
Zoom meeting 472 648 284 - - contact to join
Homotopy type theory (HoTT) is a new field of mathematics that blends logic, homotopy theory, and the theory of programming languages. In this talk, I will describe all the components of HoTT including necessary type theoretic construction. I will compare this theory with more traditional set theories like ZFC and show how homotopy theoretic constructions such as spheres and homotopy groups are defined in HoTT. I will also show how to work with such a theory in a proof assistant by providing examples of discussed concepts. Finally, I will discuss one of the open problems in the field.