The equivariant model structure on cartesian cubical sets
<|reference_start|>The equivariant model structure on cartesian cubical sets: 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.<|reference_end|>
@article{awodey2024the,
    title={The equivariant model structure on cartesian cubical sets},
    author={Steve Awodey and Evan Cavallo and Thierry Coquand and Emily Riehl and
  Christian Sattler},
    journal={arXiv preprint arXiv:2406.18497},
    year={2024},
    archivePrefix={arXiv},
    eprint={2406.18497},
    primaryClass={math.AT cs.LO math.LO}
}