Homotopy Type Theory: A Gentle Introduction

Abstract: Homotopy Type Theory (HoTT) is, syntactically, Martin-Löf Type Theory (MLTT) plus the axiom called “univalence”. Hence, it is, at the same time, an abstract functional programming language, a logical system, and a synthetic way to describe homotopy spaces. The seminar introduces the type system, focusing on the homotopy interpretation, univalence, and higher inductive types, i.e., the main novelties of HoTT with respect to MLTT. The seminar aims at providing the fundamental ideas of HoTT to mathematicians and computer scientists willing to understand what is HoTT without the burden of a formal, in-depth presentation.

Il Dott. Marco Benini è ricercatore di Logica Matematica (MAT01) del Dipartimento di Scienza e Alta Tecnologia
Università degli Studi dell’Insubria

Referente: Andrea Masini