Playing whack-a-mole with models of Homotopy Type Theory

Nicola Gambino, University of Leeds. Part of the proofs, constructions and computations seminar series.

One of the outstanding open problems in Homotopy Type Theory is that of defining a model of Martin-Löf type theory that satisfies the following three requirements: (1) the model validates Voevodsky’s univalence axiom, (2) the model is build on a category that is equivalent (in a suitable sense) to that of topological spaces, (3) the model is definable constructively, i.e. without using the law of excluded middle or the axiom of choice. Trying to solve this problem feels a lot like playing the whack-a-mole game: as soon as two problems are solved, the third one becomes harder. I will survey the current state of the art in the field, without assuming knowledge of Homotopy Type Theory, and hint at some ideas for making progress.