This formalization accompanies the article
The equivariant model structure on cartesian cubical sets.
Steve Awodey, Evan Cavallo, Thierry Coquand, Emily Riehl, and Christian Sattler.
arXiv:2406.18497.
The contents of the formalization are summarized in Appendix A of the article.
The formalization defines a model of homotopy type theory inside an extensional type theory augmented with a flat modality and axioms postulating shapes (among them an interval) and a cofibration classifier. The results can in particular be externalized in the category of cartesian cubical sets.
See index.agda for more information.
See ecavallo.github.io/equivariant-cartesian for a friendlier HTML interface.