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

{- Agda formalization for section 3 of "TOWARDS COHERENCE THEOREMS FOR
EQUATIONAL EXTENSIONS OF TYPE THEORIES" -}


{- Lib.agda
 -   Σ-types, equality types, natural numbers, ...
 -}
open import Lib


{- Fam.agda 
 -   Families, join of families, families of telescopes.
 -}
open import Fam


{- Id/Intro.agda
 -   Identity type introduction structures.
 -}
open import Id.Intro

{- Id/Elim.agda
 -   Weak identity type elimination.
 -}
open import Id.Elim

{- Id/Groupoid.agda
 -   Groupoid operations and laws.
 -}
open import Id.Groupoid

{- Id/Id.agda
 -   Other properties of identity types.
 -}
open import Id.Id

{- Id/Tele.agda
 -   Lifting identity type structures from families to joins of families and
 -   families of telescopes.
 -}
open import Id.Tele