{-# 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 9 _[_]′ʷ _[_]′ʷ : 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 9 _[_]′ᴺ _[_]′ᴺ : 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