  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 over the cartesian cube category, a well-behaved
Eilenberg-Zilber category. The key innovation is an additional equivariance
condition in the specification of the cubical Kan fibrations, which can be
described as the pullback of an interval-based class of uniform fibrations in
the category of symmetric sequences of cubical sets. The main technical results
in the development of our model have been formalized in a computer proof
assistant.
