------------------------------------------------------------------------
-- 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
import Definition.Untyped.Erased 𝕄 as Erased
open import Definition.Untyped.Neutral M type-variant
open import Definition.Typed R
open import Definition.Typed.Weakening R using (_∷ʷ_βŠ‡_)

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
    Ξ“ : Con Term n
    Ξ” : Con Term nβ€²
    ρ : 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} β†’ Con Term n β†’ (_ _ : Term n) β†’ Set β„“)
  -- Equality of terms.
  (_⊒_β‰…_∷_ : βˆ€ {n} β†’ Con Term n β†’ (_ _ _ : Term n) β†’ Set β„“)
  -- Equality of neutral terms.
  (_⊒_~_∷_ : βˆ€ {n} β†’ Con Term n β†’ (t u A : Term n) β†’ Set β„“)
  -- Are neutral cases included in the logical relation?
  (Neutrals-included : Set β„“) :
  Set β„“ where
  no-eta-equality

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

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

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

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

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

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

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

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

    -- If Neutrals-included does not hold, then definitional equality
    -- for types and terms is contained in _⊒_β‰…_ and _⊒_β‰…_∷_,
    -- respectively.
    βŠ’β‰‘β†’βŠ’β‰… :
      Β¬ Neutrals-included β†’
      Ξ“ ⊒ A ≑ B β†’ Ξ“ ⊒ A β‰… B
    βŠ’β‰‘βˆ·β†’βŠ’β‰…βˆ· :
      Β¬ Neutrals-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

    -- 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 f
           β†’ Function 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 r
          β†’ Product 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

    -- 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 universe and generic equality compatibility
  ~-to-β‰… : βˆ€ {k l lβ€²} β†’ Ξ“ ⊒ k ~ l ∷ U lβ€² β†’ Ξ“ ⊒ k β‰… l
  ~-to-β‰… k~l = β‰…-univ (~-to-β‰…β‚œ k~l)

  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 :
      ⦃ inc : Neutrals-included ⦄ β†’ Neutrals-included or-empty Ξ“
    included ⦃ inc ⦄ = possibly-nonempty ⦃ ok = inc ⦄

  opaque

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

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

  opaque

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

    with-inc-βŠ’β‰…βˆ· :
      Ξ“ ⊒ t ≑ u ∷ A β†’
      (⦃ inc : Neutrals-included ⦄ β†’ Ξ“ ⊒ t β‰… u ∷ A) β†’
      Ξ“ ⊒ t β‰… u ∷ A
    with-inc-βŠ’β‰…βˆ· t≑u tβ‰…u =
      case Neutrals-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
  field
    ---------------
    -- Relations --
    ---------------

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

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

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

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

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

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

  open Equality-relations equality-relations public