Formalization of an equivariant cartesian cubical set model of type theory

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.