Constructive aspects of simplicial homotopy theory

Dr Nicola Gambino, University of Leeds. Part of the Proofs, Constructions and Computations Seminar Series.

I will discuss some progress towards proving constructively the results of simplicial homotopy theory that allow us to define a model of Martin-Löf type theory extended with Voevodsky's univalence axiom.

This is based on joint work in progress with Simon Henry and with Christian Sattler and Karol Szumilo.