The equivariant model structure on cartesian cubical sets
Abstract
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.
Fields of Study & Subjects
Homotopy and Cohomology in Algebraic Topology
Publication details
- Journal / source
- Advances in Mathematics
- Volume
- 495
- Pages
- 110965–110965
- Publication date
- 20 April 2026
- Language
- EN