Zoom Link:

https://msri.zoom.us/s/93059090699

In joint work with Steve Awodey, Evan Cavallo, Thierry Coquand, and Christian Sattler, we introduce a constructive model for homotopy type theory on a category of cubical sets that defines a model category that is Quillen equivalent to spaces and supports "cellularly-inductive" constructions. This latter property is a feature of the cube category we use: the cartesian cube category, which is an Eilenberg-Zilber generalized Reedy category. Our model is a variation of ABCFHL obtained by demanding that the fibrations satisfy an additional equivariance condition on top of the uniform Kan condition. As a consequence, all quotients of cubes by groups of symmetries are contractible. Time permitting, we sketch the proof of the comparison Quillen equivalence, which makes heavy use of these contractible cube quotients.