From typed programming languages to synthetic homotopy theory

In this talk I'll try to give an overview of (homotopic) type theory, a theory which produces a very important link between computer science and homotopy theory and which is at the heart of modern proof assistants.

We'll start with concrete examples from computer science, which will allow us to introduce Martin-Löf's dependent type theory. We'll then talk about Voevodsky's univalence axiom and finally the interepration of this theory in simplicial sets by Voevodsky, Lumsdaine and Warren.