{-

------------------------------------------------------------------------------------------
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, & Christian Sattler.
  https://arxiv.org/abs/2406.18497

The contents of the formalization are outlined 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.

The code has been tested with Agda version 2.6.4.
The source is available at

  github.com/ecavallo/equivariant-cartesian

and there is an HTML interface at

  ecavallo.github.io/equivariant-cartesian

For reference (see the file equivariant.agda-lib in the source), the formalization is
compiled with the flags

  --with-K
  --cohesion --flat-split
  --no-import-sorts
  --rewriting

In particular, the --with-K flag enables axiom K (uniqueness of identity proofs), while
the --cohesion and --flat-split flags enable the flat modality (see the module
axiom.flat for more information).

-}

module index where

--↓ The summary module defines the interpretation of homotopy type theory: the judgments,
--↓ type formers (including universes), and the univalence axiom. Most results are
--↓ imported from elsewhere in the formalization.

import summary

--↓ The prelude: basic constructs of the ambient type theory, such as sigma types, natural
--↓ numbers, isomorphisms, etc.

import basic

--↓ Syntax for the internal model of extensional type theory where contexts are
--↓ interpreted as types and types as families in some universe.

import internal-extensional-type-theory

--↓ Axioms postulated for the construction.

import axiom

--↓ Basic properties of the cofibration classifier.

import cofibration

--↓ Consequences of the axioms expressing tinyness of shapes.

import tiny

--↓ Properties of and operations on fibrations.

import fibration

--↓ Interpretations of the type formers.

import type-former

--↓ Interpretation of the universe type and the univalence axiom.

import universe