Introduction to Homotopy Type Theory

I will give a short introduction to some recent developments in type theory, linking the intensional identity types of Martin-Lof with homotopy theory and higher-dimensional categories. The first step towards establishing such a link was made by Hoffman and Streicher, when they showed, roughly, that the intensional identity types endow every type with the structure of a groupoid. For this, they ignored nested identity proofs. They conjectured that if one would not ignore the possibility of nesting, every type would carry the structure of a (weak) infinity-groupoid. This was subsequently proved by Richard Garner and the speaker, and Peter Lumsdaine independently. It turns out that seeing types as infinity-groupoids, or homotopy types, is quite fruitful (it also lies at the basis of Voevodsky's univalent model, where types are interpreted as Kan complexes). The aim of the talk is to explain the ideas behind "homotopy type theory" and survey recent developments in this area.