{-# 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. -}