------------------------------------------------------------------------
-- An abstract set of equality relations over which the logical relation
-- is parameterized.
------------------------------------------------------------------------

open import Definition.Typed.Restrictions
open import Graded.Modality

module Definition.Typed.EqualityRelation
  {β„“} {M : Set β„“}
  {𝕄 : Modality M}
  (R : Type-restrictions 𝕄)
  where

open Type-restrictions R

open import Definition.Untyped M
open import Definition.Untyped.Whnf M type-variant
import Definition.Untyped.Erased 𝕄 as Erased
open import Definition.Typed R
open import Definition.Typed.Weakening R using (_Β»_∷ʷ_βŠ‡_)
open import Definition.Typed.Weakening.Definition R

open import Tools.Fin
open import Tools.Function
open import Tools.Level hiding (_βŠ”_)
open import Tools.Nat
open import Tools.Product
import Tools.PropositionalEquality as PE
open import Tools.Relation

private
  variable
    p q qβ€² r : M
    Ξ΄ n nβ€² l l₁ lβ‚‚ : Nat
    βˆ‡ : DCon (Term 0) n
    βˆ‡β€² : DCon (Term 0) nβ€²
    Ξ“ : Cons _ _
    Ξ” Ξ— : Con _ _
    ρ : Wk nβ€² n
    A A₁ Aβ‚‚ Aβ€² B B₁ Bβ‚‚ Bβ€² C : Term n
    a aβ€² b bβ€² e eβ€² : Term n
    m t t₁ tβ‚‚ u u₁ uβ‚‚ v v₁ vβ‚‚ w₁ wβ‚‚ : Term n
    s : Strength
    bm : BinderMode

-- If Equality-relationsΒ _⊒_β‰…_Β _⊒_β‰…_∷_Β _⊒_~_∷_ holds, then one can
-- instantiate the logical relation in Definition.LogicalRelation with
-- these relations and prove the fundamental lemma.

record Equality-relations
  -- Equality of types.
  (_⊒_β‰…_ : βˆ€ {Ξ΄ n} β†’ Cons Ξ΄ n β†’ (_ _ : Term n) β†’ Set β„“)
  -- Equality of terms.
  (_⊒_β‰…_∷_ : βˆ€ {Ξ΄ n} β†’ Cons Ξ΄ n β†’ (_ _ _ : Term n) β†’ Set β„“)
  -- Equality of neutral terms.
  (_⊒_~_∷_ : βˆ€ {Ξ΄ n} β†’ Cons Ξ΄ n β†’ (t u A : Term n) β†’ Set β„“)
  -- Are neutral cases included in the logical relation?
  (Var-included : Set β„“) :
  Set β„“ where
  no-eta-equality

  -- A variant of _⊒_β‰…_.

  infix 4 _βŠ’β‰…_

  _βŠ’β‰…_ : Cons Ξ΄ n β†’ Term n β†’ Set β„“
  Ξ“ βŠ’β‰… A = Ξ“ ⊒ A β‰… A

  -- A variant of _⊒_β‰…_∷_.

  infix 4 _βŠ’β‰…_∷_

  _βŠ’β‰…_∷_ : Cons Ξ΄ n β†’ Term n β†’ Term n β†’ Set β„“
  Ξ“ βŠ’β‰… t ∷ A = Ξ“ ⊒ t β‰… t ∷ A

  -- A variant of _⊒_~_∷_.

  infix 4 _⊒~_∷_

  _⊒~_∷_ : Cons Ξ΄ n β†’ Term n β†’ Term n β†’ Set β„“
  Ξ“ ⊒~ t ∷ A = Ξ“ ⊒ t ~ t ∷ A

  field
    -- Var-included is decided.
    Var-included? : Dec Var-included

    -- If Equality-reflection-allowed holds, then Var-included
    -- does not hold.
    Equality-reflection-allowed→¬Var-included :
      Equality-reflection β†’ Β¬ Var-included

    -- If Var-included does not hold, then definitional equality
    -- for types and terms is contained in _⊒_β‰…_ and _⊒_β‰…_∷_,
    -- respectively.
    βŠ’β‰‘β†’βŠ’β‰… :
      Β¬ Var-included β†’
      Ξ“ ⊒ A ≑ B β†’ Ξ“ ⊒ A β‰… B
    βŠ’β‰‘βˆ·β†’βŠ’β‰…βˆ· :
      Β¬ Var-included β†’
      Ξ“ ⊒ t ≑ u ∷ A β†’ Ξ“ ⊒ t β‰… u ∷ A

    -- Generic equality compatibility
    ~-to-β‰…β‚œ : Ξ“ ⊒ t ~ u ∷ A
            β†’ Ξ“ ⊒ t β‰… u ∷ A

    -- Judgmental conversion compatibility
    β‰…-eq  : Ξ“ ⊒ A β‰… B
          β†’ Ξ“ ⊒ A ≑ B
    β‰…β‚œ-eq : Ξ“ ⊒ t β‰… u ∷ A
          β†’ Ξ“ ⊒ t ≑ u ∷ A

    -- Universe
    β‰…-univ : Ξ“ ⊒ A β‰… B ∷ U l
           β†’ Ξ“ ⊒ A β‰… B

    -- Symmetry
    β‰…-sym  : Ξ“ ⊒ A β‰… B     β†’ Ξ“ ⊒ B β‰… A
    β‰…β‚œ-sym : Ξ“ ⊒ t β‰… u ∷ A β†’ Ξ“ ⊒ u β‰… t ∷ A
    ~-sym  : Ξ“ ⊒ t ~ u ∷ A β†’ Ξ“ ⊒ u ~ t ∷ A

    -- Transitivity
    β‰…-trans  : Ξ“ ⊒ A β‰… B     β†’ Ξ“ ⊒ B β‰… C     β†’ Ξ“ ⊒ A β‰… C
    β‰…β‚œ-trans : Ξ“ ⊒ t β‰… u ∷ A β†’ Ξ“ ⊒ u β‰… v ∷ A β†’ Ξ“ ⊒ t β‰… v ∷ A
    ~-trans  : Ξ“ ⊒ t ~ u ∷ A β†’ Ξ“ ⊒ u ~ v ∷ A β†’ Ξ“ ⊒ t ~ v ∷ A

    -- Conversion
    β‰…-conv : Ξ“ ⊒ t β‰… u ∷ A β†’ Ξ“ ⊒ A ≑ B β†’ Ξ“ ⊒ t β‰… u ∷ B
    ~-conv : Ξ“ ⊒ t ~ u ∷ A β†’ Ξ“ ⊒ A ≑ B β†’ Ξ“ ⊒ t ~ u ∷ B

    -- Weakening
    β‰…-wk  : βˆ‡ Β» ρ ∷ʷ Ξ— βŠ‡ Ξ”
          β†’ (βˆ‡ Β» Ξ”) ⊒ A β‰… B
          β†’ (βˆ‡ Β» Ξ—) ⊒ wk ρ A β‰… wk ρ B
    β‰…β‚œ-wk : βˆ‡ Β» ρ ∷ʷ Ξ— βŠ‡ Ξ”
          β†’ (βˆ‡ Β» Ξ”) ⊒ t β‰… u ∷ A
          β†’ (βˆ‡ Β» Ξ—) ⊒ wk ρ t β‰… wk ρ u ∷ wk ρ A
    ~-wk  : βˆ‡ Β» ρ ∷ʷ Ξ— βŠ‡ Ξ”
          β†’ (βˆ‡ Β» Ξ”) ⊒ t ~ u ∷ A
          β†’ (βˆ‡ Β» Ξ—) ⊒ wk ρ t ~ wk ρ u ∷ wk ρ A

    -- Definitional weakening
    β‰…-defn-wk  : Β» βˆ‡β€² βŠ‡ βˆ‡
               β†’ (βˆ‡ Β» Ξ”) ⊒ A β‰… B
               β†’ (βˆ‡β€² Β» Ξ”) ⊒ A β‰… B
    β‰…β‚œ-defn-wk : Β» βˆ‡β€² βŠ‡ βˆ‡
               β†’ (βˆ‡ Β» Ξ”) ⊒ t β‰… u ∷ A
               β†’ (βˆ‡β€² Β» Ξ”) ⊒ t β‰… u ∷ A
    ~-defn-wk  : Β» βˆ‡β€² βŠ‡ βˆ‡
               β†’ (βˆ‡ Β» Ξ”) ⊒ t ~ u ∷ A
               β†’ (βˆ‡β€² Β» Ξ”) ⊒ t ~ u ∷ A

    -- Weak head expansion
    β‰…-red : Ξ“ ⊒ A β†˜ Aβ€²
          β†’ Ξ“ ⊒ B β†˜ Bβ€²
          β†’ Ξ“ ⊒ Aβ€² β‰… Bβ€²
          β†’ Ξ“ ⊒ A  β‰… B

    β‰…β‚œ-red : Ξ“ ⊒ A β†˜ B
           β†’ Ξ“ ⊒ a β†˜ aβ€² ∷ B
           β†’ Ξ“ ⊒ b β†˜ bβ€² ∷ B
           β†’ Ξ“ ⊒ aβ€² β‰… bβ€² ∷ B
           β†’ Ξ“ ⊒ a  β‰… b  ∷ A

    -- Universe type reflexivity
    β‰…-Urefl   : ⊒ Ξ“ β†’ Ξ“ βŠ’β‰… U l ∷ U (1+ l)

    -- Natural number type reflexivity
    β‰…β‚œ-β„•refl : ⊒ Ξ“ β†’ Ξ“ βŠ’β‰… β„• ∷ U 0

    -- Empty type reflexivity
    β‰…β‚œ-Emptyrefl : ⊒ Ξ“ β†’ Ξ“ βŠ’β‰… Empty ∷ U 0

    -- Unit type reflexivity
    β‰…β‚œ-Unitrefl : ⊒ Ξ“ β†’ Unit-allowed s β†’ Ξ“ βŠ’β‰… Unit s l ∷ U l

    -- Unit Ξ·-equality
    β‰…β‚œ-Ξ·-unit : Ξ“ ⊒ e ∷ Unit s l
              β†’ Ξ“ ⊒ eβ€² ∷ Unit s l
              β†’ Unit-with-Ξ· s
              β†’ Ξ“ ⊒ e β‰… eβ€² ∷ Unit s l

    -- Ξ - and Ξ£-congruence

    β‰…-Ξ Ξ£-cong : βˆ€ {F G H E}
              β†’ Ξ“ ⊒ F β‰… H
              β†’ Ξ“ Β»βˆ™ F ⊒ G β‰… E
              β†’ Ξ Ξ£-allowed bm p q
              β†’ Ξ“ ⊒ ΠΣ⟨ bm ⟩ p , q β–· F β–Ή G β‰… ΠΣ⟨ bm ⟩ p , q β–· H β–Ή E

    β‰…β‚œ-Ξ Ξ£-cong
              : βˆ€ {F G H E}
              β†’ Ξ“ ⊒ F β‰… H ∷ U l₁
              β†’ Ξ“ Β»βˆ™ F ⊒ G β‰… E ∷ U lβ‚‚
              β†’ Ξ Ξ£-allowed bm p q
              β†’ Ξ“ ⊒ ΠΣ⟨ bm ⟩ p , q β–· F β–Ή G β‰… ΠΣ⟨ bm ⟩ p , q β–· H β–Ή E ∷
                  U (l₁ βŠ”α΅˜ lβ‚‚)

    -- Zero reflexivity
    β‰…β‚œ-zerorefl : ⊒ Ξ“ β†’ Ξ“ βŠ’β‰… zero ∷ β„•

    -- Successor congruence
    β‰…-suc-cong : βˆ€ {m n} β†’ Ξ“ ⊒ m β‰… n ∷ β„• β†’ Ξ“ ⊒ suc m β‰… suc n ∷ β„•

    -- Product congruence
    β‰…-prod-cong : βˆ€ {F G t tβ€² u uβ€²}
                β†’ Ξ“ Β»βˆ™ F ⊒ G
                β†’ Ξ“ ⊒ t β‰… tβ€² ∷ F
                β†’ Ξ“ ⊒ u β‰… uβ€² ∷ G [ t ]β‚€
                β†’ Ξ£Κ·-allowed p q
                β†’ Ξ“ ⊒ prodΚ· p t u β‰… prodΚ· p tβ€² uβ€² ∷ Ξ£Κ· p , q β–· F β–Ή G

    -- Ξ·-equality
    β‰…-Ξ·-eq : βˆ€ {f g F G}
           β†’ Ξ“ ⊒ f ∷ Ξ  p , q β–· F β–Ή G
           β†’ Ξ“ ⊒ g ∷ Ξ  p , q β–· F β–Ή G
           β†’ Function⁺ (Ξ“ .defs) f
           β†’ Function⁺ (Ξ“ .defs) g
           β†’ Ξ“ Β»βˆ™ F ⊒ wk1 f ∘⟨ p ⟩ var x0 β‰… wk1 g ∘⟨ p ⟩ var x0 ∷ G
           β†’ Ξ“ ⊒ f β‰… g ∷ Ξ  p , q β–· F β–Ή G

    -- Ξ· for product types
    β‰…-Ξ£-Ξ· : βˆ€ {r s F G}
          β†’ Ξ“ ⊒ r ∷ Ξ£Λ’ p , q β–· F β–Ή G
          β†’ Ξ“ ⊒ s ∷ Ξ£Λ’ p , q β–· F β–Ή G
          β†’ Product⁺ (Ξ“ .defs) r
          β†’ Product⁺ (Ξ“ .defs) s
          β†’ Ξ“ ⊒ fst p r β‰… fst p s ∷ F
          β†’ Ξ“ ⊒ snd p r β‰… snd p s ∷ G [ fst p r ]β‚€
          β†’ Ξ“ ⊒ r β‰… s ∷ Ξ£Λ’ p , q β–· F β–Ή G

    -- Variable reflexivity
    ~-var : βˆ€ {x A} β†’ Ξ“ ⊒ var x ∷ A β†’ Ξ“ ⊒~ var x ∷ A

    -- Definition reflexivity
    ~-defn : βˆ€ {Ξ± A Aβ€²}
           β†’ Ξ“ ⊒ defn Ξ± ∷ A
           β†’ Ξ± β†¦βŠ˜βˆ· Aβ€² ∈ Ξ“ .defs
           β†’ Ξ“ ⊒~ defn Ξ± ∷ A

    -- Application congruence
    ~-app : βˆ€ {a b f g F G}
          β†’ Ξ“ ⊒ f ~ g ∷ Ξ  p , q β–· F β–Ή G
          β†’ Ξ“ ⊒ a β‰… b ∷ F
          β†’ Ξ“ ⊒ f ∘⟨ p ⟩ a ~ g ∘⟨ p ⟩ b ∷ G [ a ]β‚€

    -- Product projections congruence
    ~-fst : βˆ€ {r s F G}
          β†’ Ξ“ Β»βˆ™ F ⊒ G
          β†’ Ξ“ ⊒ r ~ s ∷ Ξ£Λ’ p , q β–· F β–Ή G
          β†’ Ξ“ ⊒ fst p r ~ fst p s ∷ F

    ~-snd : βˆ€ {r s F G}
          β†’ Ξ“ Β»βˆ™ F ⊒ G
          β†’ Ξ“ ⊒ r ~ s ∷ Ξ£Λ’ p , q β–· F β–Ή G
          β†’ Ξ“ ⊒ snd p r ~ snd p s ∷ G [ fst p r ]β‚€

    -- Natural recursion congruence
    ~-natrec : βˆ€ {z zβ€² s sβ€² n nβ€² F Fβ€²}
             β†’ Ξ“ Β»βˆ™ β„• ⊒ F β‰… Fβ€²
             β†’ Ξ“ ⊒ z β‰… zβ€² ∷ F [ zero ]β‚€
             β†’ Ξ“ Β»βˆ™ β„• Β»βˆ™ F ⊒ s β‰… sβ€² ∷ F [ suc (var x1) ]↑²
             β†’ Ξ“ ⊒ n ~ nβ€² ∷ β„•
             β†’ Ξ“ ⊒ natrec p q r F z s n ~ natrec p q r Fβ€² zβ€² sβ€² nβ€² ∷
                 F [ n ]β‚€

    -- Product recursion congruence
    ~-prodrec : βˆ€ {F G A Aβ€² t tβ€² u uβ€²}
             β†’ Ξ“ Β»βˆ™ Ξ£Κ· p , q β–· F β–Ή G ⊒ A β‰… Aβ€²
             β†’ Ξ“ ⊒ t ~ tβ€² ∷ Ξ£Κ· p , q β–· F β–Ή G
             β†’ Ξ“ Β»βˆ™ F Β»βˆ™ G ⊒ u β‰… uβ€² ∷ A [ prodΚ· p (var x1) (var x0) ]↑²
             β†’ Ξ£Κ·-allowed p q
             β†’ Ξ“ ⊒ prodrec r p qβ€² A t u ~ prodrec r p qβ€² Aβ€² tβ€² uβ€² ∷
                 A [ t ]β‚€

    -- Empty recursion congruence
    ~-emptyrec : βˆ€ {n nβ€² F Fβ€²}
               β†’ Ξ“ ⊒ F β‰… Fβ€²
               β†’ Ξ“ ⊒ n ~ nβ€² ∷ Empty
               β†’ Ξ“ ⊒ emptyrec p F n ~ emptyrec p Fβ€² nβ€² ∷ F

    -- Weak unit type recursion congruence
    ~-unitrec : βˆ€ {A Aβ€² t tβ€² u uβ€²}
              β†’ Ξ“ Β»βˆ™ UnitΚ· l ⊒ A β‰… Aβ€²
              β†’ Ξ“ ⊒ t ~ tβ€² ∷ UnitΚ· l
              β†’ Ξ“ ⊒ u β‰… uβ€² ∷ A [ starΚ· l ]β‚€
              β†’ UnitΚ·-allowed
              β†’ Β¬ UnitΚ·-Ξ·
              β†’ Ξ“ ⊒ unitrec l p q A t u ~ unitrec l p q Aβ€² tβ€² uβ€² ∷
                  A [ t ]β‚€

    -- Star reflexivity
    β‰…β‚œ-starrefl : ⊒ Ξ“ β†’ Unit-allowed s β†’ Ξ“ βŠ’β‰… star s l ∷ Unit s l

    -- Id preserves "equality".
    β‰…-Id-cong
      : Ξ“ ⊒ A₁ β‰… Aβ‚‚
      β†’ Ξ“ ⊒ t₁ β‰… tβ‚‚ ∷ A₁
      β†’ Ξ“ ⊒ u₁ β‰… uβ‚‚ ∷ A₁
      β†’ Ξ“ ⊒ Id A₁ t₁ u₁ β‰… Id Aβ‚‚ tβ‚‚ uβ‚‚
    β‰…β‚œ-Id-cong
      : Ξ“ ⊒ A₁ β‰… Aβ‚‚ ∷ U l
      β†’ Ξ“ ⊒ t₁ β‰… tβ‚‚ ∷ A₁
      β†’ Ξ“ ⊒ u₁ β‰… uβ‚‚ ∷ A₁
      β†’ Ξ“ ⊒ Id A₁ t₁ u₁ β‰… Id Aβ‚‚ tβ‚‚ uβ‚‚ ∷ U l

    -- Reflexivity for rfl.
    β‰…β‚œ-rflrefl : Ξ“ ⊒ t ∷ A β†’ Ξ“ βŠ’β‰… rfl ∷ Id A t t

    -- J preserves the _⊒_~_ relation (in a certain way).
    ~-J
      : Ξ“ ⊒ A₁ β‰… Aβ‚‚
      β†’ Ξ“ ⊒ t₁ ∷ A₁
      β†’ Ξ“ ⊒ t₁ β‰… tβ‚‚ ∷ A₁
      β†’ Ξ“ Β»βˆ™ A₁ Β»βˆ™ Id (wk1 A₁) (wk1 t₁) (var x0) ⊒ B₁ β‰… Bβ‚‚
      β†’ Ξ“ ⊒ u₁ β‰… uβ‚‚ ∷ B₁ [ t₁ , rfl ]₁₀
      β†’ Ξ“ ⊒ v₁ β‰… vβ‚‚ ∷ A₁
      β†’ Ξ“ ⊒ w₁ ~ wβ‚‚ ∷ Id A₁ t₁ v₁
      β†’ Ξ“ ⊒ J p q A₁ t₁ B₁ u₁ v₁ w₁ ~ J p q Aβ‚‚ tβ‚‚ Bβ‚‚ uβ‚‚ vβ‚‚ wβ‚‚ ∷
          B₁ [ v₁ , w₁ ]₁₀

    -- K preserves the _⊒_~_ relation (in a certain way).
    ~-K
      : Ξ“ ⊒ A₁ β‰… Aβ‚‚
      β†’ Ξ“ ⊒ t₁ β‰… tβ‚‚ ∷ A₁
      β†’ Ξ“ Β»βˆ™ Id A₁ t₁ t₁ ⊒ B₁ β‰… Bβ‚‚
      β†’ Ξ“ ⊒ u₁ β‰… uβ‚‚ ∷ B₁ [ rfl ]β‚€
      β†’ Ξ“ ⊒ v₁ ~ vβ‚‚ ∷ Id A₁ t₁ t₁
      β†’ K-allowed
      β†’ Ξ“ ⊒ K p A₁ t₁ B₁ u₁ v₁ ~ K p Aβ‚‚ tβ‚‚ Bβ‚‚ uβ‚‚ vβ‚‚ ∷ B₁ [ v₁ ]β‚€

    -- If []-cong is allowed, then []-cong preserves the _⊒_~_
    -- relation (in a certain way).
    ~-[]-cong
      : Ξ“ ⊒ A₁ β‰… Aβ‚‚
      β†’ Ξ“ ⊒ t₁ β‰… tβ‚‚ ∷ A₁
      β†’ Ξ“ ⊒ u₁ β‰… uβ‚‚ ∷ A₁
      β†’ Ξ“ ⊒ v₁ ~ vβ‚‚ ∷ Id A₁ t₁ u₁
      β†’ []-cong-allowed s
      β†’ let open Erased s in
        Ξ“ ⊒ []-cong s A₁ t₁ u₁ v₁ ~ []-cong s Aβ‚‚ tβ‚‚ uβ‚‚ vβ‚‚ ∷
          Id (Erased A₁) ([ t₁ ]) ([ u₁ ])


  -- Composition of judgemental conversion and generic equality compatibility
  ~-eq : βˆ€ {k l A} β†’ Ξ“ ⊒ k ~ l ∷ A β†’ Ξ“ ⊒ k ≑ l ∷ A
  ~-eq = β‰…β‚œ-eq βˆ˜β†’ ~-to-β‰…β‚œ

  -- Composition of universe and generic equality compatibility
  ~-to-β‰… : βˆ€ {k l lβ€²} β†’ Ξ“ ⊒ k ~ l ∷ U lβ€² β†’ Ξ“ ⊒ k β‰… l
  ~-to-β‰… = β‰…-univ βˆ˜β†’ ~-to-β‰…β‚œ

  opaque

    -- A variant of β‰…β‚œ-β„•refl.

    β‰…-β„•refl : ⊒ Ξ“ β†’ Ξ“ βŠ’β‰… β„•
    β‰…-β„•refl = β‰…-univ βˆ˜β†’ β‰…β‚œ-β„•refl

  opaque

    -- A variant of β‰…β‚œ-Emptyrefl.

    β‰…-Emptyrefl : ⊒ Ξ“ β†’ Ξ“ βŠ’β‰… Empty
    β‰…-Emptyrefl = β‰…-univ βˆ˜β†’ β‰…β‚œ-Emptyrefl

  opaque

    -- A variant of β‰…β‚œ-Unitrefl.

    β‰…-Unitrefl : ⊒ Ξ“ β†’ Unit-allowed s β†’ Ξ“ βŠ’β‰… Unit s l
    β‰…-Unitrefl βŠ’Ξ“ ok = β‰…-univ (β‰…β‚œ-Unitrefl βŠ’Ξ“ ok)

  opaque

    -- A well-formedness lemma for _⊒_β‰…_.

    wf-βŠ’β‰… : Ξ“ ⊒ A β‰… B β†’ Ξ“ βŠ’β‰… A Γ— Ξ“ βŠ’β‰… B
    wf-βŠ’β‰… Aβ‰…B =
      ≅-trans A≅B (≅-sym A≅B) ,
      ≅-trans (≅-sym A≅B) A≅B

  opaque

    -- A well-formedness lemma for _⊒_β‰…_∷_.

    wf-βŠ’β‰…βˆ· : Ξ“ ⊒ t β‰… u ∷ A β†’ Ξ“ βŠ’β‰… t ∷ A Γ— Ξ“ βŠ’β‰… u ∷ A
    wf-βŠ’β‰…βˆ· tβ‰…u =
      β‰…β‚œ-trans tβ‰…u (β‰…β‚œ-sym tβ‰…u) ,
      β‰…β‚œ-trans (β‰…β‚œ-sym tβ‰…u) tβ‰…u

  opaque

    -- A well-formedness lemma for _⊒_~_∷_.

    wf-⊒~∷ : Ξ“ ⊒ t ~ u ∷ A β†’ Ξ“ ⊒~ t ∷ A Γ— Ξ“ ⊒~ u ∷ A
    wf-⊒~∷ t~u =
      ~-trans t~u (~-sym t~u) ,
      ~-trans (~-sym t~u) t~u

  opaque

    -- A variant of possibly-nonempty.

    included :
      {Ξ“ : Con Term n} ⦃ inc : Var-included ⦄ β†’
      Var-included or-empty Ξ“
    included ⦃ inc ⦄ = possibly-nonempty ⦃ ok = inc ⦄

  opaque

    -- If Ξ“Β βŠ’Β A ≑ B holds, then one can assume Var-included when
    -- proving Ξ“Β βŠ’Β AΒ β‰…Β B.

    with-inc-βŠ’β‰… :
      Ξ“ ⊒ A ≑ B β†’
      (⦃ inc : Var-included ⦄ β†’ Ξ“ ⊒ A β‰… B) β†’
      Ξ“ ⊒ A β‰… B
    with-inc-βŠ’β‰… A≑B Aβ‰…B =
      case Var-included? of Ξ» where
        (yes inc) β†’ Aβ‰…B ⦃ inc = inc ⦄
        (no ni)   β†’ βŠ’β‰‘β†’βŠ’β‰… ni A≑B

  opaque

    -- If Ξ“Β βŠ’Β t ≑ u ∷ A holds, then one can assume Var-included when
    -- proving Ξ“Β βŠ’Β tΒ β‰…Β u ∷ A.

    with-inc-βŠ’β‰…βˆ· :
      Ξ“ ⊒ t ≑ u ∷ A β†’
      (⦃ inc : Var-included ⦄ β†’ Ξ“ ⊒ t β‰… u ∷ A) β†’
      Ξ“ ⊒ t β‰… u ∷ A
    with-inc-βŠ’β‰…βˆ· t≑u tβ‰…u =
      case Var-included? of Ξ» where
        (yes inc) β†’ tβ‰…u ⦃ inc = inc ⦄
        (no ni)   β†’ βŠ’β‰‘βˆ·β†’βŠ’β‰…βˆ· ni t≑u

-- Values of type EqRelSet contain three relations that the logical
-- relation in Definition.LogicalRelation can be instantiated with.
-- The assumed properties ensure that the fundamental lemma can be
-- proved.

record EqRelSet : Set (lsuc β„“) where
  no-eta-equality
  infix 4 _⊒_β‰…_ _⊒_β‰…_∷_ _⊒_~_∷_
  field
    ---------------
    -- Relations --
    ---------------

    -- Equality of types
    _⊒_β‰…_   : Cons Ξ΄ n β†’ (A B : Term n)   β†’ Set β„“

    -- Equality of terms
    _⊒_β‰…_∷_ : Cons Ξ΄ n β†’ (t u A : Term n) β†’ Set β„“

    -- Equality of neutral terms
    _⊒_~_∷_ : Cons Ξ΄ n β†’ (t u A : Term n) β†’ Set β„“

    -- Are neutral cases included in the logical relation?
    Var-included : Set β„“

    ----------------
    -- Properties --
    ----------------

    equality-relations :
      Equality-relations _⊒_β‰…_ _⊒_β‰…_∷_ _⊒_~_∷_ Var-included

  open Equality-relations equality-relations public