{-# OPTIONS --rewriting --prop #-}

-- This Agda formalization is known to work with Agda v2.6.1.1

{- Agda formalization for some of the constructions of the paper "Coherence of
 -  strict equalities in dependent type theories".
 -}


{- Lib.agda, Quotient.agda
 -   Metatheoretic definitions (Metatheoretic Σ-types, natural numbers, equality
 -   types, quotients, etc).
 -}
open import Lib
open import Quotient


{- Fam.agda [§ 2.3, § 2.5]
 -   Internal families, join of families, families of telescopes.
 -}
open import Fam


{- Id.agda [§ 3.1]
 -   Identity type introduction structures.
 -   Weak identity type elimination.
 -   Groupoid operations and laws.
 -}
open import Id
{- Id-Tele.agda [§ 3.3]
 -   Lifting identity type structures from families to joins of families and
 -   families of telescopes.
 -}
open import Id-Tele
{- Id-Misc.agda [§ 3.4]
 -   Bidirectional identity types elimination structures.
 -   Parametrized identity types elimination structures.
 -}
open import Id-Misc
{- Id-Acyclic.agda
 -   "John Major" equality, for type families indexed by hSets.
 -}
open import Id-Acyclic


{- Pi.agda [§ 3.2]
 -   Pi type introduction structures.
 -   Pi type application structures.
 -   Several alternative definitions of Pi type extensionality structures.
 -}
open import Pi
{- Pi-Tele.agda [§ 3.3]
 -   Lifting Pi type structures from families to joins of families and families of
 -   telescopes.
 -}
open import Pi-Tele


{- Cong.agda [§ 4.4]
 -   Definition of internal congruence over a family.
 -   Lifting congruences to joins of families.
 -   Definition of the compatibility of a congruence with Id/Pi
 -}
open import Cong
{- Cong-Quotient.agda [§ 4.4]
 -   Definition of the internal quotient of an internal congruence.
 -}
open import Cong-Quotient


{- TwoLevel.agda [§ 7.2]
 -   Definition of two-level families (higher congruences) [Definition 7.1].
 - Construction of the higher congruences C⁼ [Construction 7.7]
 -   and C͌ [Construction 8.2].
 -}
open import TwoLevel
{- AcyclicTwoLevel.agda [§ 7.3]
 -   Definition of acyclic higher congruences [Definition 7.3].
 -   Construction of a congruence from an acyclic higher congruence [Construction 7.5].
 -}
open import AcyclicTwoLevel
{- AcyclicTwoLevel-Id.agda
 -   Compatibility of the congruence defined in AcyclicTwoLevel.agda with Id
 -}
open import AcyclicTwoLevel-Id
{- AcyclicTwoLevel-Pi.agda
 -   Compatibility of the congruence defined in AcyclicTwoLevel.agda with Pi
 -}
open import AcyclicTwoLevel-Pi



{- Postulates are used in the following places:
 -  - In Lib.agda, metatheoretic function extensionality and proposition
 -     extensionality are postulated.
 -  - In Quotient.agda, postulate is used to specify quotients.
 -  - In Id-Acyclic.agda, we postulate an instance of the axiom of choice that
 -     holds in our models.
 -  - In AcyclicTwoLevel-Id.agda and AcyclicTwoLevel-Pi.agda postulate is used to
 -      make an abstract copy cpi of (CPi : Pi C.Inner C.Outer), with a definitional β-rule.
 -
 - cheat is used to omit proofs in the following places:
 -  - In Id-Acyclic.agda, AcyclicTwoLevel-Id.agda and AcyclicTwoLevel-Pi.agda, cheat is used for
 -      some instance arguments, because the Agda instance resolution is too slow.
 -  - Proofs of the closure of hSets under Σ and Π are skipped.
 -}