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.