Fabian Lukas Grubmüller: A Gentle Introduction to Homotopy Type Theory

Abstract

Homotopy Type Theory (HoTT) is a field of mathematics that unifies logic, computer science, and homotopy theory. It builds upon Martin-Löf Type Theory (MLTT), reinterpreting its types as spaces and its proofs of equality as paths between points, including higher structure that arises from this interpretation. In this talk, I will first introduce the basics of MLTT, including its identity types and the principle of path induction (aka the J-rule). We will then explore the homotopical interpretation of types as ∞-groupoids, leading to the Univalence Axiom. While conceptually powerful, Univalence presents computational challenges in traditional MLTT. I will explain how modern approaches, such as Cubical Type Theory (CTT), resolve these issues. The session will conclude with a short demonstration of formalizing mathematics in Agda within a HoTT-based metatheory.