Seminar

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.

Notes 25.3 MB application/pdf

The Equivariant Uniform Kan Fibration Model Of Cubical Homotopy Type Theory