The subject of this year’s special programme at the IAS has been Univalent Foundations, aka Homotopy Type Theory — a somewhat radical new approach to working in dependent type theories (specifically, Martin- Löf’s Intensional Type Theory and relatives), informed by ideas from homotopy theory and higher category theory.

In this talk, I will briefly introduce the key ideas of the approach for those who have not seen them before, and survey the recent progress that has been made during the special year — ideas and results including new familes of axioms and type-constructors (Univalence and Higher Inductive Types), a better understanding of various existing logical constructions in the setting of Intensional Type Theory (sheaf models, gluing models, coherence theorems), and the formalisation of a large amount of homotopy theory “synthetically” in proof assistants such as Agda and Coq.