{-# OPTIONS
  --with-K --rewriting --postfix-projections --hidden-argument-puns #-}

module STT.SSC.StrictSub where

open import STT.Lib
open import Data.Product
open import Data.Product.Properties
open import STT.SSC
open import STT.SSC.SNf

private variable
  Γ Δ : Con
  γ : Sub Δ Γ
  A B C : Ty
  a b f : Tm Γ A
  x : Var Γ A

module []′ʷ where
  open NTmDModel

  M : NTmDModel _
  M .NTmᴰ Γ A a _ = ∀ {Δ γ} (γʷ : Wk Δ Γ γ) → Σ[ a′ ∈ Tm Δ A ] a [ γ ] ≡ a′
  M .NTmᴰ-prop {aᴺᴰ₀} {aᴺᴰ₁} =
    funextᵢ
      (funextᵢ
        (funext λ _ → Σ-≡,≡→≡ (sym (aᴺᴰ₀ _ .proj₂) ∙ aᴺᴰ₁ _ .proj₂ , uip _ _)))
  M .varᴺᴰ x γʷ .proj₁ = var (x [ γʷ ]ᵛʷ)
  M .varᴺᴰ x γʷ .proj₂ = var-[]ʷ γʷ
  M .appᴺᴰ fᴺᴰ aᴺᴰ γʷ .proj₁ = app (fᴺᴰ γʷ .proj₁) (aᴺᴰ γʷ .proj₁)
  M .appᴺᴰ fᴺᴰ aᴺᴰ γʷ .proj₂ =
    app-[] ∙ cong₂ app (fᴺᴰ γʷ .proj₂) (aᴺᴰ γʷ .proj₂)
  M .lamᴺᴰ bᴺᴰ γʷ .proj₁ = lam (bᴺᴰ (γʷ ⁺) .proj₁)
  M .lamᴺᴰ bᴺᴰ γʷ .proj₂ = lam-[] ∙ cong lam (bᴺᴰ (γʷ ⁺) .proj₂)

  open NTmInd M public

infixl  _[_]′ʷ
_[_]′ʷ : Tm Γ A → Wk Δ Γ γ → Tm Δ A
a [ γʷ ]′ʷ = []′ʷ.⟦ norm a ⟧ γʷ .proj₁

tm-[]′ʷ : (γʷ : Wk Δ Γ γ) → a [ γ ] ≡ a [ γʷ ]′ʷ
tm-[]′ʷ {a} γʷ = []′ʷ.⟦ norm a ⟧ γʷ .proj₂

_[_]ᵛ′ᴺᵗ : Var Γ A → NTSub Δ Γ γ → Tm Δ A
vz [ γᴺᵗ ⁺ ]ᵛ′ᴺᵗ = var vz
vs x [ γᴺᵗ ⁺ ]ᵛ′ᴺᵗ = x [ γᴺᵗ ]ᵛ′ᴺᵗ [ p ]′ʷ
vz [ ⟨_⟩ {a} _ ]ᵛ′ᴺᵗ = a
vs x [ ⟨ a ⟩ ]ᵛ′ᴺᵗ = var x

var-[]′ᴺᵗ : (γᴺᵗ : NTSub Δ Γ γ) → var x [ γ ] ≡ x [ γᴺᵗ ]ᵛ′ᴺᵗ
var-[]′ᴺᵗ {x = vz} (γᴺᵗ ⁺) = vz-⁺
var-[]′ᴺᵗ {x = vs x} (γᴺᵗ ⁺) = vs-⁺ ∙ cong _[ p ] (var-[]′ᴺᵗ γᴺᵗ) ∙ tm-[]′ʷ p
var-[]′ᴺᵗ {x = vz} ⟨ a ⟩ = vz-⟨⟩
var-[]′ᴺᵗ {x = vs x} ⟨ a ⟩ = vs-⟨⟩

module []′ᴺᵗ where
  open NTmDModel

  M : NTmDModel _
  M .NTmᴰ Γ A a _ = ∀ {Δ γ} (γᴺᵗ : NTSub Δ Γ γ) → Σ[ a′ ∈ Tm Δ A ] a [ γ ] ≡ a′
  M .NTmᴰ-prop {aᴺᴰ₀} {aᴺᴰ₁} =
    funextᵢ
      (funextᵢ
        (funext λ _ → Σ-≡,≡→≡ (sym (aᴺᴰ₀ _ .proj₂) ∙ aᴺᴰ₁ _ .proj₂ , uip _ _)))
  M .varᴺᴰ x γᴺᵗ .proj₁ = x [ γᴺᵗ ]ᵛ′ᴺᵗ
  M .varᴺᴰ x γᴺᵗ .proj₂ = var-[]′ᴺᵗ γᴺᵗ
  M .appᴺᴰ fᴺᴰ aᴺᴰ γᴺᵗ .proj₁ = app (fᴺᴰ γᴺᵗ .proj₁) (aᴺᴰ γᴺᵗ .proj₁)
  M .appᴺᴰ fᴺᴰ aᴺᴰ γᴺᵗ .proj₂ =
    app-[] ∙ cong₂ app (fᴺᴰ γᴺᵗ .proj₂) (aᴺᴰ γᴺᵗ .proj₂)
  M .lamᴺᴰ bᴺᴰ γᴺᵗ .proj₁ = lam (bᴺᴰ (γᴺᵗ ⁺) .proj₁)
  M .lamᴺᴰ bᴺᴰ γᴺᵗ .proj₂ = lam-[] ∙ cong lam (bᴺᴰ (γᴺᵗ ⁺) .proj₂)

  open NTmInd M public

_[_]′ᴺᵗ : Tm Γ A → NTSub Δ Γ γ → Tm Δ A
a [ γᴺᵗ ]′ᴺᵗ = []′ᴺᵗ.⟦ norm a ⟧ γᴺᵗ .proj₁

tm-[]′ᴺᵗ : (γᴺᵗ : NTSub Δ Γ γ) → a [ γ ] ≡ a [ γᴺᵗ ]′ᴺᵗ
tm-[]′ᴺᵗ {a} γᴺᵗ = []′ᴺᵗ.⟦ norm a ⟧ γᴺᵗ .proj₂

infixl  _[_]′ᴺ
_[_]′ᴺ : Tm Γ A → NSub Δ Γ γ → Tm Δ A
a [ wk γʷ ]′ᴺ = a [ γʷ ]′ʷ
a [ ntsub γᴺᵗ ]′ᴺ = a [ γᴺᵗ ]′ᴺᵗ

tm-[]′ᴺ : (γᴺ : NSub Δ Γ γ) → a [ γ ] ≡ a [ γᴺ ]′ᴺ
tm-[]′ᴺ (wk γʷ) = tm-[]′ʷ γʷ
tm-[]′ᴺ (ntsub γᴺᵗ) = tm-[]′ᴺᵗ γᴺᵗ

_[_]′ : Tm Γ A → Sub Δ Γ → Tm Δ A
a [ γ ]′ = a [ normˢ γ ]′ᴺ

tm-[]′ : a [ γ ] ≡ a [ γ ]′
tm-[]′ {γ} = tm-[]′ᴺ (normˢ γ)

var-p′ : var x [ p ]′ ≡ (Tm (Γ ▹ A) B ∋ var (vs x))
var-p′ = refl

vz-⟨⟩′ : var vz [ ⟨ a ⟩ ]′ ≡ a
vz-⟨⟩′ = refl

vs-⟨⟩′ : var (vs x) [ ⟨ a ⟩ ]′ ≡ var x
vs-⟨⟩′ = refl

vz-p-⁺′ : var vz [ p ⁺ ]′ ≡ (Tm (Δ ▹ A ▹ B) B ∋ var vz)
vz-p-⁺′ = refl

vz-⟨⟩-⁺′ : var vz [ ⟨ a ⟩ ⁺ ]′ ≡ (Tm (Δ ▹ B) B ∋ var vz)
vz-⟨⟩-⁺′ = refl

vs-p-⁺ : var (vs x) [ p ⁺ ]′ ≡ (Tm (Δ ▹ A ▹ B) C ∋ var x [ p ]′ [ p ]′)
vs-p-⁺ = refl

vs-⟨⟩-⁺ : var (vs x) [ ⟨ a ⟩ ⁺ ]′ ≡ (Tm (Δ ▹ B) C ∋ var x [ ⟨ a ⟩ ]′ [ p ]′)
vs-⟨⟩-⁺ = refl

app-[]-p : app f b [ p ]′ ≡ (Tm (Γ ▹ A) C ∋ app (f [ p ]′) (b [ p ]′))
app-[]-p = refl

app-[]-⟨⟩ : app f b [ ⟨ a ⟩ ]′ ≡ app (f [ ⟨ a ⟩ ]′) (b [ ⟨ a ⟩ ]′)
app-[]-⟨⟩ = refl

lam-[]-p : lam b [ p ]′ ≡ (Tm (Γ ▹ A) (B ⇒ C) ∋ lam (b [ p ⁺ ]′))
lam-[]-p = refl

lam-[]-⟨⟩ : lam b [ ⟨ a ⟩ ]′ ≡ lam (b [ ⟨ a ⟩ ⁺ ]′)
lam-[]-⟨⟩ = refl