Logic & Set Theory Seminar: Is the simplicial model of univalent foundations constructive?
Nicola Gambino (University of Leeds)
Howard House 4th Floor Seminar Room
Working within ZFC extended with two inaccessible cardinals, Voevodsky has shown that the extension of Martin-L\”of type theory with the univalence axiom admits a model in the category of simplicial sets. Later, Coquand observed that there are unavoidable obstructions to defining this model constructively, and thus decided to focus on a different model, based on cubical sets. Yet, in joint work with Christian Sattler, it is shown that it is possible to develop a variant of the simplicial model constructively, i.e. avoiding excluded middle and the axiom of choice, by working with algebraic counterparts of Kan fibrations. I will give an overview of these ideas, accessible to non-specialists in type theory or homotopy theory.