Over the past few years, deep and surprising connections have emerged between type theory and homotopy theory. These links provide a previously unavailable topological intuition for working with type theories and are at the heart of Voevodsky's Univalent Foundations of Mathematics programme. This programme seeks to develop a new approach to the development of mathematics, on the basis of type theories that include axioms motivated by homotopy theory, such as the Univalence Axiom, with an associated formalisation within proof assistants based on type theory, such as Coq and Adga. Ongoing research in this area involves also the links between homotopy theory and higher-dimensional category theory that have been intensively developed in recent years. 

This conference aims at bringing together leading experts in type theory and homotopy theory, as well as interested researchers from related areas such as mathematical logic, theoretical computer science and category theory, to exchange the latest results and ideas, and to set out directions for further exploration of the subject.  The conference is timed to serve also as a venue for presenting the advances made during the special year on Univalent Foundations at the Institute for Advanced Study.