{-|
This module defines the logical relations for values and expressions
as described in section 7.4, and proves the fundamental property (Theorem 7.1)
and the adequacy theorem (Theorem 7.2).
-}

{-# OPTIONS --safe #-}
module CtxTyp.Denotational.Adequacy where

open import Data.Bool using (Bool; true; false; if_then_else_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; suc; zero; _≥‴_; ≤‴-refl; ≤‴-step)
open import Data.Product as P using (∃-syntax; Σ-syntax; _×_;  -,_; proj₁; proj₂)
open import Data.Unit using (⊤; tt)
open import Function using (id; _∘_; case_of_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; cong₂) renaming (subst to cast)

open import CtxTyp.Context
open import CtxTyp.Term
open import CtxTyp.Term.Properties
open import CtxTyp.Depth
open import CtxTyp.Substitution
open import CtxTyp.Substitution.Properties
open import CtxTyp.Reduction
open import CtxTyp.Denotational

-- | Value and Expression Relations
𝕍 : {e : Term n (inject₁ Γ) A} → Value e → ⟦ A ⟧ Γ → Set
𝔼 : (e : Term n (inject₁ Γ) A) (d : ⟦ A ⟧ Γ) → Set

𝕍 {Γ = Γ} (`λ⟨ Δ ⟩ e₁) f = ∀ {Γ′} (σ : inject₁ Γ′ ⊩ inject₁ Γ) (e₂ : Term _ (inject₁ Γ′ ++ inject₁ Δ) _) (ve₂ : Value e₂) d →
  𝕍 ve₂ d → 𝔼 (subst (σ , term e₂) e₁) (f (⊩-inject₁⁻ σ) d)
𝕍 (`wrap Δ e ve) d = 𝕍 ve d
𝕍 `true true = ⊤
𝕍 `false false = ⊤
𝕍 `false true = ⊥
𝕍 `true false = ⊥
𝕍 ⟨ e ⟩ d = rename (∋-inject₁⁻ ∘ ∋-↾⁻) e ≡ d

𝔼 e d = ∃[ e′ ] Σ[ ve′ ∈ Value e′ ] e -→* e′ × 𝕍 ve′ d

-- | Environment Relation
𝔾 : inject₁ Γ ⊩ Δ → G⟦ Δ ⟧ Γ → Set
𝔾Item : inject₁ Γ ⊩[ Δ ⊢ A ^ m≥n ] → Item⟦ Δ ⊢ A ^ m≥n ⟧ Γ → Set

𝔾 ∅ tt = ⊤
𝔾 (σ , item) (γ P., item′) = 𝔾 σ γ × 𝔾Item item item′
𝔾 (σ₁ ++ˢ σ₂) (γ₁ P., γ₂) = 𝔾 σ₁ γ₁ × 𝔾 σ₂ γ₂

𝔾Item {Γ = Γ} {Δ = Δ} {m≥n = ≤‴-refl} (term e) f = ∀ {Γ′} (σ″ : inject₁ Γ′ ⊩ inject₁ Γ) (σ′ : inject₁ Γ′ ⊩ Δ) γ′ → (σ′~γ′ : 𝔾 σ′ γ′) → 𝔼 (subst (σ″ ++ˢ σ′) e) (f (⊩-inject₁⁻ σ″) γ′)
𝔾Item {m≥n = ≤‴-refl} (var x) f = ⊥
𝔾Item {m≥n = ≤‴-step _} item item′ = ⊩[]-inject₁⁻ item ≡ item′

-- | Compatibility of the 𝔼 relation
-→*-𝔼 : ∀ {e e′ : Term n (inject₁ Γ) A} {d} → e -→* e′ → 𝔼 e′ d → 𝔼 e d
-→*-𝔼 e-→*e′ (e″ P., ve″ P., e′-→*e″ P., ve″~d) = e″ P., ve″ P., -→*-trans e-→*e′ e′-→*e″ P., ve″~d

-- | 𝕍 is a subrelation of 𝔼
𝕍⇒𝔼 : ∀ (e : Term n (inject₁ Γ) A) (ve : Value e) {d} → 𝕍 ve d → 𝔼 e d
𝕍⇒𝔼 e ve ve~d = e P., ve P., -→*-refl P., ve~d

ext𝔾↾ : ∀ {Γ : Context n} {σ : inject₁ Γ′ ⊩ Γ} {γ} → 𝔾 σ γ → exts↾ σ ≡ renameSubst (∋-↾⁺ ∘ ∋-inject₁⁺) (γ ↾ᴳ)
ext𝔾↾ {σ = ∅} {γ = tt} tt = refl 
ext𝔾↾ {σ = _,_ {m≥n = ≤‴-refl} σ (term e)} {γ = γ P., d} (σ~γ P., e~d) = ext𝔾↾ σ~γ
ext𝔾↾ {Γ′ = Γ′} {σ = _,_ {m≥n = ≤‴-step m≥n} σ (term e)} {γ = γ P., item′} (σ~γ P., refl) =
  cong₂ _,_ (ext𝔾↾ σ~γ) (cong term (trans (sym (rename-id e))
    (trans (rename-resp-≗ (λ {
      (L x) → cong L (trans (sym (ext↾≥-id m≥n x)) (trans (ext↾≥-resp-≗ m≥n (λ x → sym (∋-↾⁺-∋-inject₁⁺-∋-inject₁⁻-∋-↾⁻ {xs = Γ′} x)) x) (ext↾≥-∘ m≥n _ _ x)));
      (R x) → refl } ) e) (rename-∘ _ _ e))))
ext𝔾↾ {σ = _,_ {m≥n = ≤‴-step m≥n} σ (var x)} {γ = γ P., item′} (σ~γ P., refl) = cong₂ _,_ (ext𝔾↾ σ~γ) (cong var (cong ∋-↾⁺ (sym (∋-inject₁⁺-∋-inject₁⁻ x))))
ext𝔾↾ {σ = σ₁ ++ˢ σ₂} {γ = γ₁ P., γ₂} (σ₁~γ₁ P., σ₂~γ₂) = cong₂ _++ˢ_ (ext𝔾↾ σ₁~γ₁) (ext𝔾↾ σ₂~γ₂)

ext𝔾↾′ : ∀ {Γ : Context n} {σ : inject₁ Γ′ ⊩ Γ} {γ} → 𝔾 σ γ → renameSubst (∋-inject₁⁻ ∘ ∋-↾⁻) (exts↾ σ) ≡ (γ ↾ᴳ)
ext𝔾↾′ σ~γ = trans (cong (renameSubst (∋-inject₁⁻ ∘ ∋-↾⁻)) (ext𝔾↾ σ~γ)) (trans (trans (sym (renameSubst-∘ _ _ _)) (renameSubst-resp-≗ ∋-inject₁⁻-∋-↾⁻-∋-↾⁺-∋-inject₁⁺ _)) (renameSubst-id _))

lookup𝔾 : ∀ {Γ : Context n} {σ : inject₁ Γ′ ⊩ Γ} {γ} → 𝔾 σ γ → ∀ {m} {Δ′} {A} {m≥n : m ≥‴ n} (x : Γ ∋[ Δ′ ⊢ A ^ m≥n ]) → 𝔾Item (lookup σ x) (lookupG γ x)
lookup𝔾 {σ = (- , σZ)} {γ = (_ P., γZ)} (_ P., σZ~γZ) Z = σZ~γZ
lookup𝔾 {σ = (σ , _)} {γ = (γ P., _)} (σ~γ P., _) (S x) = lookup𝔾 σ~γ x
lookup𝔾 {σ = (σ ++ˢ _)} {γ = (γ P., _)} (σ~γ P., _) (L x) = lookup𝔾 σ~γ x
lookup𝔾 {σ = (_  ++ˢ σ)} {γ = (_ P., γ)} (_ P., σ~γ) (R x) = lookup𝔾 σ~γ x

𝔼-castˡ : ∀ {e e′ : Term n (inject₁ Γ) A} {d} → e ≡ e′ → 𝔼 e d → 𝔼 e′ d
𝔼-castˡ refl = id

𝔼-cast² : ∀ {e e′ : Term n (inject₁ Γ) A} {d d′} → e ≡ e′ → d ≡ d′ → 𝔼 e d → 𝔼 e′ d′
𝔼-cast² refl refl = id

-- | 𝕍 relation respects later-stage substitution
𝕍-substᵈ : ∀ {σ : inject₁ Γ ⊩ inject₁ Δ} {d′} (σᵈ : σ ≤ᵈ′ d′) {e : inject₁ Δ ⊢ A ^ n} (ve : Value e) (d : ⟦ A ⟧ Δ) (ve~d : 𝕍 ve d)
  → 𝕍 (Value-substᵈ σᵈ ve) (subst⟦ A ⟧ (⊩-inject₁⁻ σ) d)
𝕍-substᵈ {σ = σ} σᵈ (`λ⟨ Δ′ ⟩ e₁) f ve₁~f = λ σ′ e₂ ve₂ d ve₂~d →
  𝔼-cast²
    (trans (subst-, (substSubst σ′ σ) (term e₂) e₁)
      (trans (cong (λ σ″ → subst σ″ e₁ [ e₂ ]) (exts-substSubst σ′ σ))
        (trans (cong (_[ e₂ ]) (subst-substSubst  (exts σ′) (exts σ) e₁))
          (trans (sym (subst-, σ′ (term e₂) (subst (exts σ) e₁)))
            (cong (subst (σ′ , term e₂)) (substᵈ-constant (exts σ) e₁)))))) 
    (cong₂ f (⊩-inject₁⁻-substSubst σ′ σ) refl)
    (ve₁~f (substSubst σ′ σ) e₂ ve₂ d ve₂~d)
𝕍-substᵈ σᵈ `true true .tt = tt
𝕍-substᵈ σᵈ `false false .tt = tt
𝕍-substᵈ {σ = σ} σᵈ ⟨ e ⟩ d refl =
  trans (sym (substᵈ-renameSubstᵈ (∋-inject₁⁻ ∘ ∋-↾⁻) _ e))
    (trans (substᵈ-cong (sym (⊩-inject₁⁻≡exts↾ σ)) e)
      (trans (substᵈ-constant (renameSubstʳ (∋-inject₁⁻ ∘ ∋-↾⁻) (⊩-inject₁⁻ σ)) e)
        (substᵈ-renameSubstʳᵈ (∋-inject₁⁻ ∘ ∋-↾⁻) (≤ᵈ′-refl (⊩-inject₁⁻ σ)) e)))
𝕍-substᵈ {σ = σ} σᵈ (`wrap {A = A} Δ′ e ve) d ve~d =
  cast (𝕍 (Value-substᵈ (exts++ᵈ (inject₁ Δ′) σᵈ) ve))
    (cong₂ subst⟦ A ⟧ (⊩-inject₁⁻-exts++ σ) refl)
    (𝕍-substᵈ (exts++ᵈ (inject₁ Δ′) σᵈ) ve d ve~d) 

𝔾-substᵈ : ∀ {Δ : Context n} {σ : inject₁ Γ′ ⊩ inject₁ Γ} {d′} (σᵈ : σ ≤ᵈ′ d′) (σ₁ : inject₁ Γ ⊩ Δ) (γ₁ : G⟦ Δ ⟧ Γ) (σ₁~γ₁ : 𝔾 σ₁ γ₁)
  → 𝔾 (substSubstᵈ σᵈ σ₁) (substG (⊩-inject₁⁻ σ) γ₁)
𝔾-substᵈ σᵈ ∅ tt tt = tt
𝔾-substᵈ {σ = σ} σᵈ (_,_ {Δ = Δ′} {m≥n = ≤‴-refl} σ₁ (term e)) (γ₁ P., f) (σ₁~γ₁ P., e~f) = 𝔾-substᵈ σᵈ σ₁ γ₁ σ₁~γ₁ P., λ σ″ σ′ γ′ σ′~γ′ →
  𝔼-cast²
    (trans (subst-++ˢ (substSubst σ″ σ) σ′ e)
      (trans (cong (subst (lift id ++ˢ σ′))
        (trans (cong (λ σ‴ → subst σ‴ e) (exts++-substSubst σ″ σ))
          (subst-substSubst  (exts++ Δ′ σ″) (exts++ Δ′ σ) e)))
        (trans (sym (subst-++ˢ σ″ σ′ (subst (exts++ Δ′ σ) e)))
          (cong (subst (σ″ ++ˢ σ′)) (substᵈ-constant (exts++ Δ′ σ) e)))))
    (cong₂ f (⊩-inject₁⁻-substSubst σ″ σ) refl)
    (e~f (substSubst σ″ σ) σ′ γ′ σ′~γ′)
𝔾-substᵈ {σ = σ} σᵈ (_,_ {m≥n = ≤‴-step m≥n} σ₁ item) (γ₁ P., _) (σ₁~γ₁ P., refl) = 𝔾-substᵈ σᵈ σ₁ γ₁ σ₁~γ₁ P., trans (cong ⊩[]-inject₁⁻ (substSubstItemᵈ-constant σ item)) (⊩[]-inject₁⁻-substSubstItem σ item)
𝔾-substᵈ σᵈ (σ₁ ++ˢ σ₂) (γ₁ P., γ₂) (σ₁~γ₁ P., σ₂~γ₂) = 𝔾-substᵈ σᵈ σ₁ γ₁ σ₁~γ₁ P., 𝔾-substᵈ σᵈ σ₂ γ₂ σ₂~γ₂

𝕍-subst : ∀ (σ : inject₁ Γ ⊩ inject₁ Δ) {e : inject₁ Δ ⊢ A ^ n} (ve : Value e) (d : ⟦ A ⟧ Δ) (ve~d : 𝕍 ve d)
  → 𝕍 (Value-subst σ ve) (subst⟦ A ⟧ (⊩-inject₁⁻ σ) d)
𝕍-subst σ = 𝕍-substᵈ (≤ᵈ′-refl σ)

𝔾-subst : ∀ {Δ : Context n} (σ : inject₁ Γ′ ⊩ inject₁ Γ) {σ₁ : inject₁ Γ ⊩ Δ} {γ₁ : G⟦ Δ ⟧ Γ} (σ₁~γ₁ : 𝔾 σ₁ γ₁)
  → 𝔾 (substSubst σ σ₁) (substG (⊩-inject₁⁻ σ) γ₁)
𝔾-subst σ = 𝔾-substᵈ (≤ᵈ′-refl σ) _ _

𝔾-lift : (ρ : Rename {n = n} (inject₁ Γ) (inject₁ Γ′)) → 𝔾 (lift ρ) (liftG (Rename-inject₁⁻ ρ))
𝔾-lift {Γ = ∅} ρ = tt
𝔾-lift {Γ = Γ ,[ x ^ m≥n ]} ρ = 𝔾-lift (ρ ∘ S) P., refl
𝔾-lift {Γ = Γ₁ ++ Γ₂} ρ = 𝔾-lift (ρ ∘ L) P., 𝔾-lift (ρ ∘ R)

𝔾-cast² : ∀ {Δ : Context n} {σ σ′ : inject₁ Γ ⊩ Δ} {γ γ′} → (eq₁ : σ ≡ σ′) (eq₂ : γ ≡ γ′) → 𝔾 σ γ → 𝔾 σ′ γ′
𝔾-cast² refl refl = id

𝔾-exts++ : (Δ : Context (suc n)) → ∀ {σ : inject₁ Γ′ ⊩ Γ} {γ} → 𝔾 σ γ → 𝔾 (exts++ (inject₁ Δ) σ) (extG++ Δ γ)
𝔾-exts++ Δ {σ = σ} {γ = γ} σ~γ = 𝔾-cast² (substSubst-lift L σ) (cong (λ σ′ → substG σ′ γ) (trans (⊩-inject₁⁻-lift L) (lift-resp-≗ Rename-inject₁⁻-L))) (𝔾-subst (lift L) σ~γ) P., 𝔾-cast² refl (liftG-resp-≗ Rename-inject₁⁻-R) (𝔾-lift R)

single𝕍 : ∀ {e : inject₁ Γ ++ inject₁ Δ ⊢ A ^ n} (ve : Value e) (d : ⟦ A ⟧ (Γ ++ Δ)) → 𝕍 ve d
  → ∀ {Γ′} (σ′ : inject₁ Γ′ ⊩ inject₁ Γ) (σ : inject₁ Γ′ ⊩ inject₁ Δ) → (γ : G⟦ inject₁ Δ ⟧ Γ′) → 𝔾 σ γ
  → 𝔼 (subst (σ′ ++ˢ σ) e) (single⟦ A ⟧ d (⊩-inject₁⁻ σ′) γ)
single𝕍 {A = A} ve d ve~d σ′ σ γ σ~γ = 
  𝔼-cast² refl
    (cong (λ σ″ → subst⟦ A ⟧ (⊩-inject₁⁻ σ′ ++ˢ σ″) d) (trans (⊩-inject₁⁻≡exts↾′ σ) (cong (renameSubstʳ (∋-↾⁺ ∘ ∋-inject₁⁺)) (ext𝔾↾′ σ~γ))))
    (𝕍⇒𝔼 _ (Value-subst (σ′ ++ˢ σ) ve) (𝕍-subst (σ′ ++ˢ σ) ve d ve~d))

-- | The fundamental property
fund : ∀ (e : Term n Γ A) (σ : inject₁ Γ′ ⊩ Γ) γ → 𝔾 σ γ → 𝔼 (subst σ e) (E⟦ e ⟧ γ)
fundS : ∀ {Δ : Context n} (σ₁ : Γ ⊩ Δ) (σ : inject₁ Γ′ ⊩ Γ) γ → 𝔾 σ γ → 𝔾 (substSubst σ σ₁) (S⟦ σ₁ ⟧ γ)

-- Variables
fund (` x `with σ₁) σ γ σ~γ with lookup σ x | lookupᵈ (≤ᵈ′-refl σ) x | lookup𝔾 σ~γ x
... | var y | _ | _ = ⊥-elim (inject₁-∌-refl y)
... | term e | term-Δ<d | σx~γx with depthSubst σ | ≤ᵈ′-refl σ
... | suc d′ | _ =
  𝔼-cast²
    (trans (cong (λ σσ′ → subst (lift id ++ˢ σσ′) e) (substSubstᵈ-constant σ σ₁)) (substᵈ-constant (lift id ++ˢ substSubstᵈ _ σ₁) e))
    (cong (λ σ″ → lookupG γ x σ″ (S⟦ σ₁ ⟧ γ)) ⊩-inject₁⁻-lift-id)
    (σx~γx (lift id) (substSubst σ σ₁) (S⟦ σ₁ ⟧ γ) (fundS σ₁ σ γ σ~γ))

-- Booleans
fund `true σ γ σ~γ = -, `true P., -→*-refl P., tt
fund `false σ γ σ~γ = -, `false P., -→*-refl P., tt
fund (`if e₁ `then e₂ `else e₃) σ γ σ~γ with E⟦ e₁ ⟧ γ | fund e₁ σ γ σ~γ
... | true | _ P., `true P., e₁-→*true P., tt = -→*-𝔼 (-→*-trans (ξ-if₁* e₁-→*true) (-→*-step β-if-true -→*-refl)) (fund e₂ σ γ σ~γ)
... | false | _ P., `false P., e₁-→*false P., tt = -→*-𝔼 (-→*-trans (ξ-if₁* e₁-→*false) (-→*-step β-if-false -→*-refl)) (fund e₃ σ γ σ~γ)

-- Functions
fund (`λ⟨_⟩_ {A = A} Δ  e₁) σ γ σ~γ = subst σ (`λ⟨ Δ ⟩ e₁) P., `λ⟨ Δ ⟩ _ P., -→*-refl P., λ σ′ e₂ ve₂ d ve₂~d →
  𝔼-castˡ
    (trans (subst-, (substSubst σ′ σ) (term e₂) e₁)
      (trans (cong (λ σ″ → subst σ″ e₁ [ e₂ ]) (exts-substSubst σ′ σ))
        (trans (cong (_[ e₂ ]) (subst-substSubst (exts σ′) (exts σ) e₁))
          (trans (sym (subst-, σ′ (term e₂) (subst (exts σ) e₁)))
            (cong (subst (σ′ , term e₂)) (substᵈ-constant (exts σ) e₁))))))
    (fund e₁ (substSubst σ′ σ , term e₂) (substG (⊩-inject₁⁻ σ′) γ P., single⟦ A ⟧ d) (𝔾-subst σ′ σ~γ P., single𝕍 ve₂ d ve₂~d))
fund (_·_ {Δ = Δ} e₁ e₂) σ γ σ~γ with
  _ P., ve₁@(`λ⟨ .Δ ⟩ e₁′)  P., e₁-→*λ⟨⟩e₁′ P., f ← fund e₁ σ γ σ~γ |
  e₂′ P., ve₂′ P., e₂-→*e₂′ P., ve₂′~d ← fund e₂ (exts++ (inject₁ Δ) σ) (extG++ Δ γ) (𝔾-exts++ Δ σ~γ) =
  -→*-𝔼
    (-→*-trans (ξ-·₁*  e₁-→*λ⟨⟩e₁′) (-→*-trans (ξ-·₂* ve₁ (-→*-trans (-→*-reflexive (substᵈ-constant (exts++ (inject₁ Δ) σ) e₂)) e₂-→*e₂′)) (-→*-step (β-λ⟨⟩· ve₂′) -→*-refl)))
    (𝔼-cast²
      (trans (subst-, (lift id) (term e₂′) e₁′) (cong (_[ e₂′ ]) (trans (cong (λ σ → subst σ e₁′) exts-lift-id) (subst-lift-id e₁′))))
      (cong₂ (E⟦ e₁ ⟧ γ) ⊩-inject₁⁻-lift-id refl)
      (f (lift id) e₂′ ve₂′ (E⟦ e₂ ⟧ (extG++ Δ γ)) ve₂′~d))

-- Quotes
fund {Γ′ = Γ′} ⟨ e ⟩ σ γ σ~γ  = -, ⟨ substᵈ (exts↾ᵈ (≤ᵈ′-refl σ)) e ⟩ P., -→*-refl P.,
  trans (sym (substᵈ-renameSubstᵈ _ _ e))
    (trans (substᵈ-constant (renameSubst (∋-inject₁⁻ ∘ ∋-↾⁻) (exts↾ σ)) e)
      (cong (λ σ′ → subst σ′ e) (ext𝔾↾′ σ~γ)))
fund {Γ′ = Γ′} (`let⟨ Δ ⟩ e₁ e₂) σ γ σ~γ with E⟦ e₁ ⟧ (extG++ Δ γ) | fund e₁ (exts++ (inject₁ Δ) σ) (extG++ Δ γ) (𝔾-exts++ Δ σ~γ)
... | e | _ P., ⟨ e₁′ ⟩  P., e₁-→*⟨e₁′⟩ P., refl =
  -→*-𝔼
    (-→*-trans
      (ξ-let⟨⟩₁* (-→*-trans
          (-→*-reflexive (substᵈ-constant (exts++ (inject₁ Δ) σ) e₁))
          e₁-→*⟨e₁′⟩))
      (-→*-step β-let⟨⟩ -→*-refl)) 
    (𝔼-castˡ
      (trans (subst-, σ _ e₂)
        (trans (cong (λ e₁″ → subst (exts σ) e₂ [ e₁″ ]) (trans (sym (rename-∘ _ _ e₁′)) (rename-resp-≗ (λ { (L x) → cong L (∋-↾⁺-∋-inject₁⁺-∋-inject₁⁻-∋-↾⁻ {xs = Γ′} x); (R x) → refl }) e₁′)))
          (cong (_[ _ ]) (substᵈ-constant (exts σ) e₂))))
      (fund e₂ (σ , term (rename (ext++ Δ (∋-↾⁺ ∘ ∋-inject₁⁺)) e)) (γ P., term e) (σ~γ P.,  cong term
        (trans (sym (rename-∘  _ _ e))
          (trans
            (rename-resp-≗ (λ {
              (L x) → cong L (∋-inject₁⁻-∋-↾⁻-∋-↾⁺-∋-inject₁⁺ x);
              (R x) → refl }) e)
            (rename-id e))))))

-- Wraps
fund (`wrap Δ e) σ γ σ~γ with fund e (exts++ (inject₁ Δ) σ) (extG++ Δ γ) (𝔾-exts++ Δ σ~γ)
... | e′ P., ve′ P., e-→*e′ P., ve′~d = -, `wrap Δ e′ ve′ P., ξ-wrap* (-→*-trans (-→*-reflexive (substᵈ-constant _ e)) e-→*e′) P., ve′~d
fund (`letwrap {A = A} Δ e₁ e₂) σ γ σ~γ with E⟦ e₁ ⟧ γ | fund e₁ σ γ σ~γ
... | d | _ P., `wrap .Δ e₁′ ve₁′ P., e₁-→*e₁′ P., ve₁′~d =
  -→*-𝔼
    (-→*-trans (ξ-letwrap₁* e₁-→*e₁′) (-→*-step (β-letwrap (`wrap Δ e₁′ ve₁′)) -→*-refl))
    (𝔼-castˡ 
      (trans (subst-, σ (term e₁′) e₂) (cong _[ e₁′ ] (substᵈ-constant (exts σ) e₂)))
      (fund e₂ (σ , term e₁′) (γ P., single⟦ A ⟧ d) (σ~γ P., single𝕍 ve₁′ d ve₁′~d)))

-- Substitutions
fundS ∅ σ γ σ~γ = tt
fundS {Δ = Δ ,[ Δ′ ⊢ A ^ ≤‴-refl ]} (σ₁ , term e) σ γ σ~γ = fundS σ₁ σ γ σ~γ P., λ σ″ σ′ γ′ σ′~γ′ →
  𝔼-castˡ
    (trans (subst-++ˢ (substSubst σ″ σ) σ′ e)
      (trans (cong (subst (lift id ++ˢ σ′))
        (trans (cong (λ σ‴ → subst σ‴ e) (exts++-substSubst σ″ σ))
          (subst-substSubst  (exts++ Δ′ σ″) (exts++ Δ′ σ) e)))
        (trans (sym (subst-++ˢ σ″ σ′ (subst (exts++ Δ′ σ) e)))
          (cong (subst (σ″ ++ˢ σ′)) (substᵈ-constant (exts++ Δ′ σ) e)))))
    (fund e (substSubst σ″ σ ++ˢ σ′) (substG (⊩-inject₁⁻ σ″) γ ∪ γ′) (𝔾-subst σ″ σ~γ P., σ′~γ′))
fundS {Γ′ = Γ′} {Δ = Δ ,[ Δ′ ⊢ A ^ ≤‴-step m≥n ]} (σ₁ , term e) σ γ σ~γ = fundS σ₁ σ γ σ~γ P.,
  cong term
    (trans (sym (substᵈ-renameSubstᵈ (ext++ Δ′ (ext↾≥ m≥n (∋-inject₁⁻ ∘ ∋-↾⁻))) (exts++ᵈ _ (exts↾≥ᵈ (≤‴-step m≥n) (≤ᵈ′-refl σ))) e))
      (trans (substᵈ-cong (trans (sym (exts++-renameSubst _ _ _)) (cong (exts++ _) (trans (sym (exts↾≥-renameSubst m≥n _ _)) (cong (exts↾≥ m≥n) (ext𝔾↾′ σ~γ))))) e)
        (substᵈ-constant (exts++ Δ′ (exts↾≥ m≥n (γ ↾ᴳ))) e)))
fundS {Δ = Δ ,[ Δ′ ⊢ A ^ ≤‴-refl ]} (σ₁ , var x) σ γ σ~γ with lookup σ x | lookup𝔾 σ~γ x
... | term e | σx~γx = fundS σ₁ σ γ σ~γ P., σx~γx
... | var y | _ = ⊥-elim (inject₁-∌-refl y)
fundS {Δ = Δ ,[ Δ′ ⊢ A ^ ≤‴-step m≥n ]} (σ₁ , var x) σ γ σ~γ = fundS σ₁ σ γ σ~γ P., lookup𝔾 σ~γ x
fundS {Δ = Δ₁ ++ Δ₂} (σ₁ ++ˢ σ₂) σ γ σ~γ = fundS σ₁ σ γ σ~γ P., fundS σ₂ σ γ σ~γ

-- | Termination of -→* is a consequence of the fundamental lemma
-→*-terminating : ∀ (e : Term n (inject₁ Γ) A) → ∃[ e′ ] Σ[ ve′ ∈ Value e′ ] e -→* e′
-→*-terminating e 
  using e′ P., ve′ P., e-→*e′ P., _ ← fund e (lift id) (liftG id) (𝔾-cast² refl (liftG-resp-≗ Rename-inject₁⁻-id) (𝔾-lift id))
  = e′ P., ve′ P., -→*-trans (-→*-reflexive (sym (subst-lift-id e))) e-→*e′

-- | Adequacy of the denotational semantics for booleans
adequacy-`Bool : (e : Term n (inject₁ Γ) `Bool) → e -→* (if eval e then `true else `false)
adequacy-`Bool e with eval e | fund e (lift id) (liftG id) (𝔾-cast² refl (liftG-resp-≗ Rename-inject₁⁻-id) (𝔾-lift id))
... | true | `true P., `true P., e-→*`true P., _ = -→*-trans (-→*-reflexive (sym (subst-lift-id e))) e-→*`true
... | false | `false P., `false P., e-→*`false P., _ = -→*-trans (-→*-reflexive (sym (subst-lift-id e))) e-→*`false

-- | Adequacy of the denotational semantics for code types
adequacy-◯ : ∀ (e : Term n (inject₁ Γ) (◯ A)) → e -→* ⟨ rename (∋-↾⁺ ∘ ∋-inject₁⁺) (eval e) ⟩
adequacy-◯ {Γ = Γ} e with eval e | fund e (lift id) (liftG id) (𝔾-cast² refl (liftG-resp-≗ Rename-inject₁⁻-id) (𝔾-lift id))
... | _ | ⟨ e′ ⟩ P., ⟨ _ ⟩ P., e-→*⟨e′⟩ P., refl =
  -→*-trans (-→*-reflexive (sym (subst-lift-id e)))
    (-→*-trans e-→*⟨e′⟩
      (-→*-reflexive (cong ⟨_⟩ (trans (sym (trans (rename-resp-≗ (∋-↾⁺-∋-inject₁⁺-∋-inject₁⁻-∋-↾⁻ {xs = Γ}) e′) (rename-id e′))) (rename-∘ (∋-↾⁺ ∘ ∋-inject₁⁺) (∋-inject₁⁻ ∘ ∋-↾⁻) e′)))))