{-# OPTIONS --without-K --safe #-}

open import Level
open import Axiom.Extensionality.Propositional

-- Semantic judgments for substitutions
module Cumulative.Soundness.Substitutions (fext : Extensionality 0ℓ (suc 0ℓ)) where

open import Lib
open import Data.Nat.Properties

open import Cumulative.Statics.Properties
open import Cumulative.Semantics.Properties.PER fext
open import Cumulative.Soundness.Cumulativity fext
open import Cumulative.Soundness.LogRel
open import Cumulative.Soundness.ToSyntax fext
open import Cumulative.Soundness.Contexts fext
open import Cumulative.Soundness.Properties.LogRel fext
open import Cumulative.Soundness.Properties.Substitutions fext


s-I′ : ⊩ Γ →
       ------------
       Γ ⊩s I ∶ Γ
s-I′ ⊩Γ = record
  { ⊩Γ   = ⊩Γ
  ; ⊩Γ′  = ⊩Γ
  ; krip = helper
  }
  where helper : Δ ⊢s σ ∶ ⊩Γ ® ρ → GluSubst Δ I ⊩Γ σ ρ
        helper {ρ = ρ} σ∼ρ = record
          { ⟦τ⟧    = ρ
          ; ↘⟦τ⟧   = ⟦I⟧
          ; τσ∼⟦τ⟧ = s®-resp-s≈ ⊩Γ σ∼ρ (s-≈-sym (I-∘ (s®⇒⊢s ⊩Γ σ∼ρ)))
          }

s-wk′ : ⊩ T ∷ Γ →
        ------------------
        T ∷ Γ ⊩s wk ∶ Γ
s-wk′ ⊩TΓ@(⊩∷ ⊩Γ ⊢T gT) = record
  { ⊩Γ   = ⊩TΓ
  ; ⊩Γ′  = ⊩Γ
  ; krip = helper
  }
  where helper : Δ ⊢s σ ∶ ⊩TΓ ® ρ → GluSubst Δ wk ⊩Γ σ ρ
        helper {ρ = ρ} σ∼ρ = record
          { ⟦τ⟧    = drop ρ
          ; ↘⟦τ⟧   = ⟦wk⟧
          ; τσ∼⟦τ⟧ = s®-resp-s≈ ⊩Γ step (s-≈-sym ≈pσ)
          }
          where open Glu∷ σ∼ρ

s-∘′ : Γ ⊩s τ ∶ Γ′ →
       Γ′ ⊩s σ ∶ Γ″ →
       ----------------
       Γ ⊩s σ ∘ τ ∶ Γ″
s-∘′ {_} {τ} {_} {σ} ⊩τ ⊩σ = record
  { ⊩Γ   = ⊩τ.⊩Γ
  ; ⊩Γ′  = ⊩σ.⊩Γ′
  ; krip = helper
  }
  where module ⊩τ = _⊩s_∶_ ⊩τ
        module ⊩σ = _⊩s_∶_ ⊩σ
        ⊢τ = ⊩s⇒⊢s ⊩τ
        ⊢σ = ⊩s⇒⊢s ⊩σ
        helper : Δ ⊢s σ′ ∶ ⊩τ.⊩Γ ® ρ → GluSubst Δ (σ ∘ τ) ⊩σ.⊩Γ′ σ′ ρ
        helper {_} {σ′} {ρ} σ′∼ρ = record
          { ⟦τ⟧    = σ.⟦τ⟧
          ; ↘⟦τ⟧   = ⟦∘⟧ τ.↘⟦τ⟧ σ.↘⟦τ⟧
          ; τσ∼⟦τ⟧ = s®-resp-s≈ ⊩σ.⊩Γ′ σ.τσ∼⟦τ⟧ (s-≈-sym (∘-assoc ⊢σ ⊢τ (s®⇒⊢s ⊩τ.⊩Γ σ′∼ρ)))
          }
          where module τ = GluSubst (⊩τ.krip σ′∼ρ)
                module σ = GluSubst (⊩σ.krip (s®-irrel ⊩τ.⊩Γ′ ⊩σ.⊩Γ τ.τσ∼⟦τ⟧))

s-,′ : ∀ {i} →
       Γ ⊩s σ ∶ Δ →
       Δ ⊩ T ∶ Se i →
       Γ ⊩ t ∶ T [ σ ] →
       -------------------
       Γ ⊩s σ , t ∶ T ∷ Δ
s-,′ {_} {σ} {Δ} {T} {t} {i} ⊩σ ⊩T ⊩t = record
  { ⊩Γ   = ⊩σ.⊩Γ
  ; ⊩Γ′  = ⊩TΔ
  ; krip = helper
  }
  where module ⊩σ = _⊩s_∶_ ⊩σ
        module ⊩T = _⊩_∶_ ⊩T
        module ⊩t = _⊩_∶_ ⊩t
        ⊢σ  = ⊩s⇒⊢s ⊩σ
        ⊢t  = ⊩⇒⊢-tm ⊩t
        ⊢T  = ⊩⇒⊢-tm ⊩T
        ⊩TΔ = ⊢∷′ ⊩T
        ⊢TΔ = ⊩⇒⊢ ⊩TΔ
        helper : Δ′ ⊢s τ ∶ ⊩σ.⊩Γ ® ρ → GluSubst Δ′ (σ , t) ⊩TΔ τ ρ
        helper {Δ′} {τ} {ρ} τ∼ρ
          with ⊩σ.krip τ∼ρ
             | ⊩t.krip (s®-irrel ⊩σ.⊩Γ ⊩t.⊩Γ τ∼ρ)
        ...  | στ@record { ⟦τ⟧ = ⟦τ⟧ ; ↘⟦τ⟧ = ↘⟦τ⟧ ; τσ∼⟦τ⟧ = τσ∼⟦τ⟧ }
             | record { ⟦T⟧ = ⟦T⟧ ; ⟦t⟧ = ⟦t⟧ ; ↘⟦T⟧ = ⟦[]⟧ ↘ρ′ ↘⟦T⟧ ; ↘⟦t⟧ = ↘⟦t⟧ ; T∈𝕌 = T∈𝕌 ; t∼⟦t⟧ = t∼⟦t⟧ }
             rewrite ⟦⟧s-det ↘ρ′ ↘⟦τ⟧
             with s®-irrel ⊩σ.⊩Γ′ ⊩T.⊩Γ τσ∼⟦τ⟧
        ...     | τσ∼⟦τ⟧′
                with ⊩T.krip τσ∼⟦τ⟧′ | s®-cons ⊩TΔ τσ∼⟦τ⟧′
        ...        | record { ↘⟦T⟧ = ⟦Se⟧ .i ; ↘⟦t⟧ = ↘⟦T⟧′ ; T∈𝕌 = U i<l _ ; t∼⟦t⟧ = T∼⟦T⟧ } | cons
                   rewrite Glu-wellfounded-≡ i<l
                         | ⟦⟧-det ↘⟦T⟧′ ↘⟦T⟧ = record
                     { ⟦τ⟧    = ⟦τ⟧ ↦ ⟦t⟧
                     ; ↘⟦τ⟧   = ⟦,⟧ ↘⟦τ⟧ ↘⟦t⟧
                     ; τσ∼⟦τ⟧ = record
                       { ⊢σ   = ⊢σtτ
                       ; pσ   = ∷.pσ
                       ; v0σ  = ∷.v0σ
                       ; ⟦T⟧  = ∷.⟦T⟧
                       ; ≈pσ  = ≈pσ
                       ; ≈v0σ = ≈-trans (≈-conv ([]-cong (v-≈ ⊢TΔ here) eq₁) (≈-trans ([∘]-Se ⊢T (s-wk ⊢TΔ) ⊢σtτ) ([]-cong-Se″ ⊢T ≈pσ))) ∷.≈v0σ
                       ; ↘⟦T⟧ = ∷.↘⟦T⟧
                       ; T∈𝕌  = ∷.T∈𝕌
                       ; t∼ρ0 = ∷.t∼ρ0
                       ; step = ∷.step
                       }
                     }
          where module T = GluU T∼⟦T⟧
                ⊢τ   = s®⇒⊢s ⊩σ.⊩Γ τ∼ρ
                ⊢σ,t = s-, ⊢σ ⊢T ⊢t
                ⊢σtτ = s-∘ ⊢τ ⊢σ,t
                module ∷ = Glu∷ (cons (®El-master T∈𝕌 T.A∈𝕌 T.A∈𝕌 T.rel t∼⟦t⟧ ([∘]-Se ⊢T ⊢σ ⊢τ)))

                eq₁ = ,-∘ ⊢σ ⊢T ⊢t ⊢τ
                eq₂ = ∘-cong eq₁ (wk-≈ ⊢TΔ)
                ≈pσ = s-≈-trans eq₂ ∷.≈pσ

s-conv′ : Γ ⊩s σ ∶ Δ →
          ⊢ Δ ≈ Δ′ →
          -------------
          Γ ⊩s σ ∶ Δ′
s-conv′ {_} {σ} ⊩σ Δ≈Δ′ = record
  { ⊩Γ   = ⊩σ.⊩Γ
  ; ⊩Γ′  = ⊩Δ′
  ; krip = helper
  }
  where module ⊩σ = _⊩s_∶_ ⊩σ
        ⊩Δ′ = ⊩-resp-≈ ⊩σ.⊩Γ′ Δ≈Δ′
        helper : Δ″ ⊢s τ ∶ ⊩σ.⊩Γ ® ρ → GluSubst Δ″ σ ⊩Δ′ τ ρ
        helper {_} {τ} τ∼ρ = record
          { ⟦τ⟧    = ⟦τ⟧
          ; ↘⟦τ⟧   = ↘⟦τ⟧
          ; τσ∼⟦τ⟧ = s®-resp-≈′ ⊩σ.⊩Γ′ ⊩Δ′ τσ∼⟦τ⟧ Δ≈Δ′
          }
          where open GluSubst (⊩σ.krip τ∼ρ)