Logic seminar

Introduction to homotopy type theory

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.