The equivariant model structure on cartesian cubical sets

Steve Awodey, Evan Cavallo, Thierry Coquand +2

We develop a constructive model of homotopy type theory in a Quillen model category that classically presents the usual homotopy theory of spaces. Our model is based on presheaves…