------------------------------------------------------------------------
-- 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.Neutral M type-variant
open import Definition.Typed R hiding (_,_)
open import Definition.Typed.Weakening R using (_∷_βŠ‡_)

import Graded.Derived.Erased.Untyped 𝕄 as Erased

open import Tools.Fin
open import Tools.Function
open import Tools.Level
open import Tools.Nat
open import Tools.Relation

private
  variable
    p q qβ€² r : M
    n nβ€² : 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
    k l m t t₁ tβ‚‚ u u₁ uβ‚‚ v v₁ vβ‚‚ w₁ wβ‚‚ : Term n
    s : Strength
    bm : BinderMode

-- Generic equality relation used with the logical relation

record EqRelSet : Set (lsuc β„“) where
  constructor eqRel
  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 β„“

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

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

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

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

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

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

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

    -- Weakening
    β‰…-wk  : ρ ∷ Ξ” βŠ‡ Ξ“
          β†’ ⊒ Ξ”
          β†’ Ξ“ ⊒ A β‰… B
          β†’ Ξ” ⊒ wk ρ A β‰… wk ρ B
    β‰…β‚œ-wk : ρ ∷ Ξ” βŠ‡ Ξ“
          β†’ ⊒ Ξ”
          β†’ Ξ“ ⊒ t β‰… u ∷ A
          β†’ Ξ” ⊒ wk ρ t β‰… wk ρ u ∷ wk ρ A
    ~-wk  : ρ ∷ Ξ” βŠ‡ Ξ“
          β†’ ⊒ Ξ”
          β†’ Ξ“ ⊒ k ~ l ∷ A
          β†’ Ξ” ⊒ wk ρ k ~ wk ρ l ∷ 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 β‰… U

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

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

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

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

    -- Ξ - and Ξ£-congruence

    β‰…-Ξ Ξ£-cong : βˆ€ {F G H E}
              β†’ Ξ“ ⊒ F
              β†’ Ξ“ ⊒ 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
              β†’ Ξ“ ⊒ F β‰… H ∷ U
              β†’ Ξ“ βˆ™ F ⊒ G β‰… E ∷ U
              β†’ Ξ Ξ£-allowed bm p q
              β†’ Ξ“ ⊒ ΠΣ⟨ bm ⟩ p , q β–· F β–Ή G β‰… ΠΣ⟨ bm ⟩ p , q β–· H β–Ή E ∷ U

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

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

    -- Product congruence
    β‰…-prod-cong : βˆ€ {F G t tβ€² u uβ€²}
                β†’ Ξ“ ⊒ F
                β†’ Ξ“ βˆ™ 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
           β†’ Ξ“ ⊒ 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}
          β†’ Ξ“ ⊒ F
          β†’ Ξ“ βˆ™ 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 ~ 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
          β†’ Ξ“ βˆ™ F ⊒ G
          β†’ Ξ“ ⊒ r ~ s ∷ Ξ£Λ’ p , q β–· F β–Ή G
          β†’ Ξ“ ⊒ fst p r ~ fst p s ∷ F

    ~-snd : βˆ€ {r s F G}
          β†’ Ξ“ ⊒ F
          β†’ Ξ“ βˆ™ 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 β‰… 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β€²}
             β†’ Ξ“                      ⊒ F
             β†’ Ξ“ βˆ™ F                  ⊒ G
             β†’ Ξ“ βˆ™ (Ξ£Κ· 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Κ· ⊒ A β‰… Aβ€²
              β†’ Ξ“ ⊒ t ~ tβ€² ∷ UnitΚ·
              β†’ Ξ“ ⊒ u β‰… uβ€² ∷ A [ starΚ· ]β‚€
              β†’ UnitΚ·-allowed
              β†’ Β¬ UnitΚ·-Ξ·
              β†’ Ξ“ ⊒ unitrec p q A t u ~ unitrec p q Aβ€² tβ€² uβ€² ∷ A [ t ]β‚€

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

    -- 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
      β†’ Ξ“ ⊒ t₁ β‰… tβ‚‚ ∷ A₁
      β†’ Ξ“ ⊒ u₁ β‰… uβ‚‚ ∷ A₁
      β†’ Ξ“ ⊒ Id A₁ t₁ u₁ β‰… Id Aβ‚‚ tβ‚‚ uβ‚‚ ∷ U

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

    -- J preserves the _⊒_~_ relation (in a certain way).
    ~-J
      : Ξ“ ⊒ A₁
      β†’ Ξ“ ⊒ 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₁ ∷ 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} β†’ Ξ“ ⊒ k ~ l ∷ U β†’ Ξ“ ⊒ 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 β‰… Empty
    β‰…-Emptyrefl = β‰…-univ βˆ˜β†’ β‰…β‚œ-Emptyrefl

  opaque

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

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