module Semantics.Relation where

open import Prelude
open import Setoid
open import WSLN
open import ETT

----------------------------------------------------------------------
-- The graphs of the semantic functions for terms, variables, types
-- and contexts
----------------------------------------------------------------------
infix 3
  ⟦_⊢[_]_tm⟧＝
  ⟦_⊢[_]_vr⟧＝
  ⟦_⊢[_]_ty⟧＝
  ⟦_cx⟧＝

-- Terms
data ⟦_⊢[_]_tm⟧＝ (Γ : Cx) :
  (l : Lvl)
  (a : Tm)
  (CTt : ∑[ C ∈ Uω ] ∑ (Fam l C) (Elt l C))
  → ----------------------------------------
  Set

-- Variables
data ⟦_⊢[_]_vr⟧＝ :
  (Γ : Cx)
  (l : Lvl)
  (x : 𝔸)
  (CTt : ∑[ C ∈ Uω ] ∑ (Fam l C) (Elt l C))
  → ----------------------------------------
  Set

-- Types
⟦_⊢[_]_ty⟧＝ :
  (Γ : Cx)
  (l : Lvl)
  (A : Ty)
  (CT : ∑ Uω (Fam l))
  → ------------------
  Set

(⟦ Γ ⊢[ l ] A ty⟧＝(C , T)) =
  -- types are treated as a special case of terms
  -- using fam-as-elt
  ⟦ Γ ⊢[ 1+ l ] A tm⟧＝ (C , 𝒰𝓃𝒾𝓋 l , T)

-- Contexts
data ⟦_cx⟧＝ :
  (Γ : Cx)
  (C : Uω)
  → -------
  Set

data ⟦_⊢[_]_tm⟧＝ Γ where
  resp⟦tm⟧ :
    {l : Lvl}
    {a : Tm}
    {CTt CTt' : ∑[ C ∈ Uω ] ∑(Fam l C) (Elt l C)}
    (_ : ⟦ Γ ⊢[ l ] a tm⟧＝ CTt)
    (_ : Σℰ𝓁𝓉 l ∋ CTt ~ CTt')
    → --------------------------------------------
    ⟦ Γ ⊢[ l ] a tm⟧＝ CTt'

  ⟦𝐔⟧ :
    {l : Lvl}
    {C : Uω}
    (q : ⟦ Γ cx⟧＝ C)
    → ----------------------------------
    ⟦ Γ ⊢[ 1+ l ] 𝐔 l ty⟧＝ (C , 𝒰𝓃𝒾𝓋 l)

  ⟦𝚷⟧ :
    {l l' : Lvl}
    {A : Ty}
    {B : Ty[ 1 ]}
    {C : Uω}
    {S : Fam l C}
    {T : Fam l' (C ⋉[ l ] S)}
    (X : Fset𝔸)
    (q₀ : ⟦ Γ ⊢[ l ] A ty⟧＝ (C , S))
    (q₁ : ∀ x → x # X →
      ⟦ Γ ⨟ x ∶ A ⦂ l ⊢[ l' ] B [ x ] ty⟧＝(C ⋉[ l ] S , T))
    → ------------------------------------------------------
     ⟦ Γ ⊢[ max l l' ] (𝚷 l l' A B) ty⟧＝ (C , 𝒫𝒾 l l' S T)


  ⟦𝐄𝐪⟧ :
    {l : Lvl}
    {A : Ty}
    {a a' : Tm}
    {C : Uω}
    {T : Fam l C}
    {t t' : Elt l C T}
    (q₀ : ⟦ Γ ⊢[ l ] A ty⟧＝(C , T))
    (q₁ : ⟦ Γ ⊢[ l ] a tm⟧＝(C , T , t))
    (q₂ : ⟦ Γ ⊢[ l ] a' tm⟧＝(C , T , t'))
    → --------------------------------------------
    ⟦ Γ ⊢[ l ] (𝐄𝐪 A a a') ty⟧＝ (C , ℰ𝓆 l T t t')

  ⟦𝐍𝐚𝐭⟧ :
    {C : Uω}
    (q : ⟦ Γ cx⟧＝ C)
    → ----------------------------
    ⟦ Γ ⊢[ 0 ] 𝐍𝐚𝐭 ty⟧＝ (C , 𝒩𝒶𝓉)

  ⟦𝐯⟧ :
    {l : Lvl}
    {x : 𝔸}
    {CTt : ∣ Σℰ𝓁𝓉 l ∣}
    (q : ⟦ Γ ⊢[ l ] x vr⟧＝ CTt)
    → --------------------------
    ⟦ Γ ⊢[ l ] 𝐯 x tm⟧＝ CTt

  ⟦𝛌⟧ :
    {l l' : Lvl}
    {A : Ty}
    {b : Tm[ 1 ]}
    {C : Uω}
    {S : Fam l C}
    {T : Fam l' (C ⋉[ l ] S)}
    {t : Elt l' (C ⋉[ l ] S) T}
    (X : Fset𝔸)
    (q₀ : ⟦ Γ ⊢[ l ] A ty⟧＝(C , S))
    (q₁ : ∀ x → x # X →
      ⟦ Γ ⨟ x ∶ A ⦂ l ⊢[ l' ] b [ x ] tm⟧＝
      (C ⋉[ l ] S , T , t))
    → ------------------------------------
    ⟦ Γ ⊢[ max l l' ] (𝛌 A b)  tm⟧＝
      (C , 𝒫𝒾 l l' S T , 𝓁𝒶𝓂 l l' S t)

  ⟦∙⟧ :
    {l l' : Lvl}
    {A : Ty}
    {B : Ty[ 1 ]}
    {a b : Tm}
    {C : Uω}
    {S : Fam l C}
    {T : Fam l' (C ⋉[ l ] S)}
    {t : Elt (max l l' ) C (𝒫𝒾 l l' S T)}
    {s : Elt l C S}
    (X : Fset𝔸)
    (q₀ : ⟦ Γ ⊢[ max l l' ] b tm⟧＝
      (C , 𝒫𝒾 l l' S T , t))
    (q₁ : ⟦ Γ ⊢[ l ] A ty⟧＝(C , S))
    (q₂ : ∀ x → x # X →
      ⟦ Γ ⨟ x ∶ A ⦂ l ⊢[ l' ] B [ x ] ty⟧＝
      (C ⋉[ l ] S , T))
    (q₃ : ⟦ Γ ⊢[ l ] a tm⟧＝(C , S , s))
    → -------------------------------------
    ⟦ Γ ⊢[ l' ] (b ∙[ A , B ] a) tm⟧＝
    (C , ⟪ s ⟫ * T , 𝒶𝓅𝓅 l l' S T t s)

  ⟦𝐫𝐞𝐟𝐥⟧ :
    {l : Lvl}
    {A : Ty}
    {a : Tm}
    {C : Uω}
    {T : Fam l C}
    {t : Elt l C T}
    (q₀ : ⟦ Γ ⊢[ l ] A ty⟧＝(C , T))
    (q₁ : ⟦ Γ ⊢[ l ] a tm⟧＝(C , T , t))
    → ----------------------------------
    ⟦ Γ ⊢[ l ] (𝐫𝐞𝐟𝐥 A a) tm⟧＝
      (C , ℰ𝓆 l T t t , 𝓇𝒻𝓁 l T t)

  ⟦𝐳𝐞𝐫𝐨⟧ :
    {C : Uω}
    (q : ⟦ Γ cx⟧＝ C)
    → -------------------------------------
    ⟦ Γ ⊢[ 0 ] 𝐳𝐞𝐫𝐨 tm⟧＝ (C , 𝒩𝒶𝓉 , 𝓏ℯ𝓇ℴ)

  ⟦𝐬𝐮𝐜𝐜⟧ :
    {a : Tm}
    {C : Uω}
    {t : Elt 0 C 𝒩𝒶𝓉}
    (q : ⟦ Γ ⊢[ 0 ] a  tm⟧＝(C , 𝒩𝒶𝓉 , t))
    → -----------------------------------------
    ⟦ Γ ⊢[ 0 ] 𝐬𝐮𝐜𝐜 a tm⟧＝ (C , 𝒩𝒶𝓉 , 𝓈𝓊𝒸𝒸 t)

  ⟦𝐧𝐫𝐞𝐜⟧ :
    {l : Lvl}
    {B : Ty[ 1 ]}
    {b₀ a : Tm}
    {b₊ : Tm[ 2 ]}
    {C : Uω}
    {S : Fam l (C ⋉[ 0 ] 𝒩𝒶𝓉)}
    {s₀ : Elt l C (⟪ 𝓏ℯ𝓇ℴ ⟫ * S)}
    {s₊ : Elt l (C ⋉[ 0 ] 𝒩𝒶𝓉 ⋉[ l ] S)
      (𝓅 S * 𝒸ℴ𝓃𝓈 (𝓅 𝒩𝒶𝓉) (𝓈𝓊𝒸𝒸 (𝓆 𝒩𝒶𝓉)) * S)}
    {s : Elt 0 C 𝒩𝒶𝓉}
    (X : Fset𝔸)
    (q₀ : ∀ x → x # X →
      ⟦ Γ ⨟ x ∶ 𝐍𝐚𝐭 ⦂ 0 ⊢[ l ] B [ x ] ty⟧＝
      (C ⋉[ 0 ] 𝒩𝒶𝓉 , S))
    (q₁ : ⟦ Γ ⊢[ l ] b₀ tm⟧＝ (C , ⟪ 𝓏ℯ𝓇ℴ ⟫ * S , s₀))
    (q₂ : ∀ x y → x # y # X →
      ⟦ Γ ⨟ x ∶ 𝐍𝐚𝐭 ⦂ 0 ⨟ y ∶ B [ x ] ⦂ l ⊢[ l ]
      b₊ [ x ][ y ] tm⟧＝
        (C ⋉[ 0 ] 𝒩𝒶𝓉 ⋉[ l ] S ,
         𝓅 S * 𝒸ℴ𝓃𝓈 (𝓅 𝒩𝒶𝓉) (𝓈𝓊𝒸𝒸 (𝓆 𝒩𝒶𝓉)) * S , s₊))
    (q₃ : ⟦ Γ ⊢[ 0 ] a tm⟧＝(C , 𝒩𝒶𝓉 , s))
    → -----------------------------------------------
    ⟦ Γ ⊢[ l ] (𝐧𝐫𝐞𝐜 B b₀ b₊ a) tm⟧＝
      (C ,  ⟪ s ⟫ * S , 𝓃𝓇ℯ𝒸 l S s₀ s₊ s)

data ⟦_⊢[_]_vr⟧＝ where
  resp⟦vr⟧ :
    {l : Lvl}
    {Γ : Cx}
    {x : 𝔸}
    {CTt CTt' : ∑[ C ∈ Uω ] ∑ (Fam l C) (Elt l C)}
    (_ : ⟦ Γ ⊢[ l ] x vr⟧＝ CTt)
    (_ : Σℰ𝓁𝓉 l ∋ CTt  ~ CTt')
    → ---------------------------------------------
    ⟦ Γ ⊢[ l ] x vr⟧＝ CTt'

  ⟦new⟧ :
    {l : Lvl}
    {Γ : Cx}
    {A : Ty}
    {C : Uω}
    {T : Fam l C}
    {x : 𝔸}
    (q₀ : ⟦ Γ ⊢[ l ] A ty⟧＝(C , T))
    (q₁ : x # Γ)
    → -------------------------------
    ⟦ Γ ⨟ x ∶ A ⦂ l ⊢[ l ] x vr⟧＝
      (C ⋉[ l ] T , 𝓅 T * T , 𝓆 T)

  ⟦old⟧ :
    {l l' : Lvl}
    {Γ : Cx}
    {A' : Ty}
    {C : Uω}
    {T : Fam l C}
    {T' : Fam l' C}
    {t : Elt l C T}
    {x x' : 𝔸}
    (q₀ : ⟦ Γ ⊢[ l' ] A' ty⟧＝(C , T'))
    (q₁ : ⟦ Γ ⊢[ l ] x vr⟧＝(C , T , t))
    (q₂ : x' # Γ)
    → ------------------------------------
    ⟦ Γ ⨟ x' ∶ A' ⦂ l' ⊢[ l ] x vr⟧＝
    (C ⋉[ l' ] T' , 𝓅 T' * T , 𝓅 T' *₁ t)

data ⟦_cx⟧＝ where
  ⟦◇⟧ : ⟦ ◇ cx⟧＝ Unit

  ⟦⨟⟧ :
    {l : Lvl}
    {Γ : Cx}
    {A : Ty}
    {C : Uω}
    {T : Fam l C}
    {x : 𝔸}
    (q₀ : ⟦ Γ ⊢[ l ] A ty⟧＝(C , T))
    (q₁ : x # Γ)
    → -------------------------------
    ⟦ Γ ⨟ x ∶ A ⦂ l cx⟧＝(C ⋉[ l ] T)

-- The "respectfulness" properties for types and contexts are
-- derivable:
resp⟦ty⟧ :
  {Γ : Cx}
  {l : Lvl}
  {A : Ty}
  {CT CT' : ∑ Uω (Fam l)}
  (_ : ⟦ Γ ⊢[ l ] A ty⟧＝ CT)
  (_ : Σℱ𝒶𝓂 l ∋ CT ~ CT')
  → ------------------------
  ⟦ Γ ⊢[ l ] A ty⟧＝ CT'

resp⟦ty⟧ q (e , e') = resp⟦tm⟧ q (e , (λ _ _ _ → tt) , e')

resp⟦cx⟧ :
  {Γ : Cx}
  {C C' : Uω}
  (_ : ⟦ Γ cx⟧＝ C)
  (_ : 𝒰ω ∋ C ~ C')
  → ----------------
  ⟦ Γ cx⟧＝ C'

resp⟦cx⟧ {C' = Unit} ⟦◇⟧ yy = ⟦◇⟧
resp⟦cx⟧ {C' = Sigma _ _ _ _} (⟦⨟⟧ q₀ q₁) (e , refl , e') =
  ⟦⨟⟧ (resp⟦ty⟧ q₀ (e , e')) q₁