On the simplicial and cubical models of univalent foundations
Nicola Gambino ( University of Leeds )
As shown by Voevodsky, Martin-Löf type theory extended with the univalence axiom admits a model in the category of simplicial sets, which is defined within classical set theory. In an effort to prove Voevodsky's canonicity conjecture, Coquand and his collaborators have developed constructive counterparts of the simplicial model. This work involves two main aspects: moving from simplicial sets to cubical sets and working with algebraic variants of the notion of a Kan fibration. The aim of the seminar is to give a survey of the simplicial and cubical models and describe the motivations for some recent work done by Christian Sattler and Andrew Swan in Leeds.