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

open import Level
open import Axiom.Extensionality.Propositional

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

open import Lib
open import Data.Nat.Properties

open import MLTT.Statics.Properties
open import MLTT.Semantics.Properties.PER fext
open import MLTT.Soundness.Cumulativity fext
open import MLTT.Soundness.LogRel
open import MLTT.Soundness.ToSyntax fext
open import MLTT.Soundness.Contexts fext
open import MLTT.Soundness.Properties.LogRel fext
open import MLTT.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 τ∼ρ)