Expless.agda

module Expless where
 
----------------------------------------------------------------------

infixr 4 _,_
infixr 0 _∧_

record _∧_ (A B : Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B

----------------------------------------------------------------------

open import Data.Empty
open import Data.Unit
open import Data.Product
open import Relation.Binary.PropositionalEquality

----------------------------------------------------------------------

infixr 3 _`→_

data Type : Set where
  `Bool `ℕ : Type
  _`→_ : Type → Type → Type

data Form : Set where wh nf : Form

----------------------------------------------------------------------

data Ctx : Set where
  ∅ : Ctx
  _,_ : Ctx → Type → Ctx

data Var : Ctx → Type → Set where
  here : ∀{Γ A} → Var (Γ , A) A
  there : ∀{Γ A B} → Var Γ A → Var (Γ , B) A

_++_ : (Γ Δ : Ctx) → Ctx
Γ ++ ∅ = Γ
Γ ++ (Δ , A) = (Γ ++ Δ) , A

----------------------------------------------------------------------

data Val (m : Form) : Ctx → Type → Set
data Neut (m : Form) : Ctx → Type → Set
data Env (Φ : Ctx) : Ctx → Set
data Bind : Form → Ctx → Type → Type → Set

data Bind where
  `val : ∀{Γ A B} → Val nf (Γ , A) B → Bind nf Γ A B
  _`/_ : ∀{Γ Δ A B} → Env Δ Γ → Val wh (Γ , A) B → Bind wh Δ A B

----------------------------------------------------------------------

data Val m where
  `true `false : ∀{Γ} → Val m Γ `Bool
  `zero : ∀{Γ} → Val m Γ `ℕ
  `suc : ∀{Γ} → Val m Γ `ℕ → Val m Γ `ℕ
  `λ : ∀{Γ A B} → Bind m Γ A B → Val m Γ (A `→ B)
  `neut : ∀{Γ A} (x : Neut m Γ A) → Val m Γ A

data Neut m where
  `var : ∀{Γ A} (i : Var Γ A) → Neut m Γ A
  _`∙_ : ∀{Γ A B} (f : Neut m Γ (A `→ B)) (a : Val m Γ A) → Neut m Γ B
  `if_then_else_ : ∀{Γ C} (b : Neut m Γ `Bool) (ct cf : Val m Γ C) → Neut m Γ C
  `rec : ∀{Γ C} (b : Neut m Γ `ℕ) (cz : Val m Γ C) (cs : Bind m Γ C C) → Neut m Γ C

data Env Φ where
  ∅ : Env Φ ∅
  _,_ : ∀{Γ A} → Env Φ Γ → Val wh Φ A → Env Φ (Γ , A)

----------------------------------------------------------------------

`xᴺ : ∀{m Γ A} → Neut m (Γ , A) A
`xᴺ = `var here

`x : ∀{m Γ A} → Val m (Γ , A) A
`x = `neut `xᴺ

lookup : ∀{Φ Γ A} → Env Φ Γ → Var Γ A → Val wh Φ A
lookup (σ , a) here = a
lookup (σ , a) (there i) = lookup σ i

inj-neut : ∀{m Γ A}
  {x y : Neut m Γ A}
  → `neut x ≡ `neut y
  → x ≡ y
inj-neut refl = refl

----------------------------------------------------------------------

data Ren : Ctx → Ctx → Set where
  done : Ren ∅ ∅
  skip : ∀{Φ Γ A} → Ren Φ Γ → Ren (Φ , A) Γ
  keep :  ∀{Φ Γ A} → Ren Φ Γ → Ren (Φ , A) (Γ , A)

idRen : ∀{Γ} → Ren Γ Γ
idRen {∅} = done
idRen {Γ , A} = keep idRen

----------------------------------------------------------------------

renᴿ : ∀{Γ Φ A} (σ : Ren Φ Γ) → Var Γ A → Var Φ A
renᴿ done ()
renᴿ (skip σ) i = there (renᴿ σ i)
renᴿ (keep σ) here = here
renᴿ (keep σ) (there i) = there (renᴿ σ i)

----------------------------------------------------------------------

renˢ : ∀{Φ Γ Δ} → Ren Δ Φ → Env Φ Γ → Env Δ Γ
ren : ∀{m Φ Γ A} (σ : Ren Φ Γ) → Val m Γ A → Val m Φ A
renᴺ : ∀{m Φ Γ A} (σ : Ren Φ Γ) → Neut m Γ A → Neut m Φ A
renᴮ : ∀{m Φ Γ A B} (σ : Ren Φ Γ) → Bind m Γ A B → Bind m Φ A B

renᴮ σ (`val f) = `val (ren (keep σ) f)
renᴮ σ (ρ `/ f) = renˢ σ ρ `/ f

renˢ Δ≥Φ ∅ = ∅
renˢ Δ≥Φ (σ , a) = renˢ Δ≥Φ σ , ren Δ≥Φ a

ren σ `true = `true
ren σ `false = `false
ren σ `zero = `zero
ren σ (`suc n) = `suc (ren σ n)
ren σ (`λ bnd) = `λ (renᴮ σ bnd)
ren σ (`neut n) = `neut (renᴺ σ n)

renᴺ σ (`var j) = `var (renᴿ σ j)
renᴺ σ (n `∙ a) = renᴺ σ n `∙ ren σ a
renᴺ σ (`if b then ct else cf) = `if renᴺ σ b then ren σ ct else ren σ cf
renᴺ σ (`rec n cz cs) = `rec (renᴺ σ n) (ren σ cz) (renᴮ σ cs)

----------------------------------------------------------------------

liftRen : ∀{Γ Φ} Δ → Ren Φ Γ → Ren (Φ ++ Δ) (Γ ++ Δ)
liftRen ∅ σ = σ
liftRen (Δ , A) σ = keep (liftRen Δ σ)

skipsRen : ∀{Γ Φ} Δ → Ren Φ Γ → Ren (Φ ++ Δ) Γ
skipsRen ∅ σ = σ
skipsRen (Δ , A) σ = skip (skipsRen Δ σ)

wknRen₁ : ∀{Γ A} → Ren (Γ , A) Γ
wknRen₁ = skip idRen

wknRen : ∀{Γ} Δ → Ren (Γ ++ Δ) Γ
wknRen Δ = skipsRen Δ idRen

wkn : ∀{m Γ A} → Val m Γ A → ∀ Δ → Val m (Γ ++ Δ) A
wkn x Δ = ren (wknRen Δ) x

wkn₁ : ∀{m Γ A B} → Val m Γ B → Val m (Γ , A) B
wkn₁ = ren wknRen₁

wknˢ : ∀{Γ Φ} → Env Φ Γ → ∀ Δ → Env (Φ ++ Δ) Γ
wknˢ σ Δ = renˢ (wknRen Δ) σ

wkn₁ˢ : ∀{Γ Φ A} → Env Φ Γ → Env (Φ , A) Γ
wkn₁ˢ = renˢ wknRen₁

↑₁ : ∀{Γ Δ A} → Env Δ Γ → Env (Δ , A) (Γ , A)
↑₁ σ = wkn₁ˢ σ , `x

idEnv : ∀{Γ} → Env Γ Γ
idEnv {∅} = ∅
idEnv {Γ , A} = ↑₁ idEnv

----------------------------------------------------------------------

infix 1 _/_⇓_
infix 1 _/ᴺ_⇓_
infix 1 _∘_⇓_

data _/_⇓_ {Φ Γ} (σ : Env Φ Γ) : ∀{A} → Val wh Γ A → Val wh Φ A → Set
data _/ᴺ_⇓_ {Φ Γ} (σ : Env Φ Γ) : ∀{A} → Neut wh Γ A → Val wh Φ A → Set

data _∘_⇓_ {Φ Δ} (σ : Env Φ Δ) : ∀{Γ} → Env Δ Γ → Env Φ Γ → Set where
  `comp-emp : σ ∘ ∅ ⇓ ∅

  `comp-ext : ∀{Γ A} {ρ : Env Δ Γ} {a : Val wh Δ A} {a' : Val wh Φ A} {ρ' : Env Φ Γ}
    → σ ∘ ρ ⇓ ρ'
    → σ / a ⇓ a'
    → σ ∘ ρ , a ⇓ ρ' , a'

data _/ᴮ_⇓_ {Φ Γ A B} (σ : Env Φ Γ) : Bind wh Γ A B → Bind wh Φ A B → Set where
  `sub-bind : ∀{Δ}
    {b : Val wh (Δ , A) B}
    {ρ : Env Γ Δ}
    {ρ' : Env Φ Δ}
    (pρ : σ ∘ ρ ⇓ ρ')
    → σ /ᴮ (ρ `/ b) ⇓ (ρ' `/ b)

data _//_⇓_ {Γ A B} : Bind wh Γ A B → Val wh Γ A → Val wh Γ B → Set where
  `app-bind : ∀{Δ}
    {b : Val wh (Δ , A) B}
    {b' : Val wh Γ B}
    {σ : Env Γ Δ}
    {a : Val wh Γ A}
    → σ , a / b ⇓ b'
    → (σ `/ b) // a  ⇓ b'

data rec_of_∣_⇓_ {Γ C} : Val wh Γ `ℕ → Val wh Γ C → Bind wh Γ C C → Val wh Γ C → Set where
  `rec-zero :
    {cz : Val wh Γ C}
    {cs : Bind wh Γ C C}
    → rec `zero of cz ∣ cs ⇓ cz

  `rec-suc :
    {n : Val wh Γ `ℕ}
    {cz : Val wh Γ C}
    {cs : Bind wh Γ C C}
    {c c' : Val wh Γ C}
    → rec n of cz ∣ cs ⇓ c
    → cs // c ⇓ c'
    → rec (`suc n) of cz ∣ cs ⇓ c'

  `rec-neut :
    {n : Neut wh Γ `ℕ}
    {cz : Val wh Γ C}
    {cs : Bind wh Γ C C}
    → rec `neut n of cz ∣ cs ⇓ `neut (`rec n cz cs)

----------------------------------------------------------------------

data _/_⇓_ {Φ Γ} σ where
  `sub-true : σ / `true ⇓ `true
  `sub-false : σ / `false ⇓ `false
  `sub-zero : σ / `zero ⇓ `zero

  `sub-suc :
    {n : Val wh Γ `ℕ}
    {n' : Val wh Φ `ℕ}
    → σ / n ⇓ n'
    → σ / (`suc n) ⇓ (`suc n')

  `sub-lam : ∀{A B}
    {f : Bind wh Γ A B}
    {f' : Bind wh Φ A B}
    → σ /ᴮ f ⇓ f'
    → σ / `λ f ⇓ `λ f'

  `sub-neut : ∀{B}
    {n : Neut wh Γ B}
    {n' : Val wh Φ B}
    (pn : σ /ᴺ n ⇓ n')
    → σ / `neut n ⇓ n'

----------------------------------------------------------------------

data _/ᴺ_⇓_ {Φ Γ} σ where
  `sub-var : ∀{A}
    (i : Var Γ A)
    → σ /ᴺ `var i ⇓ lookup σ i

  `sub-if-true : ∀{C}
    {b : Neut wh Γ `Bool}
    {ct cf : Val wh Γ C}
    {ct' : Val wh Φ C}
    (pb : σ /ᴺ b ⇓ `true)
    (pct : σ / ct ⇓ ct')
    → σ /ᴺ `if b then ct else cf ⇓ ct'

  `sub-if-false : ∀{C}
    {b : Neut wh Γ `Bool}
    {ct cf : Val wh Γ C}
    {cf' : Val wh Φ C}
    (pb : σ /ᴺ b ⇓ `false)
    (pcf : σ / cf ⇓ cf')
    → σ /ᴺ `if b then ct else cf ⇓ cf'

  `sub-if-neut : ∀{C}
    {b : Neut wh Γ `Bool}
    {ct cf : Val wh Γ C}
    {b' : Neut wh Φ `Bool}
    {ct' cf' : Val wh Φ C}
    (pb : σ /ᴺ b ⇓ `neut b')
    (pct : σ / ct ⇓ ct')
    (pcf : σ / cf ⇓ cf')
    → σ /ᴺ `if b then ct else cf ⇓ `neut (`if b' then ct' else cf')

  `sub-rec : ∀{C}
    {n : Neut wh Γ `ℕ}
    {n' : Val wh Φ `ℕ}
    {cz : Val wh Γ C}
    {cs : Bind wh Γ C C}
    {cz' : Val wh Φ C}
    {cs' : Bind wh Φ C C}
    {c' : Val wh Φ C}
    (n⇓n' : σ /ᴺ n ⇓ n')
    (cz⇓cz' : σ / cz ⇓ cz')
    (cs⇓cs' : σ /ᴮ cs ⇓ cs')
    → rec n' of cz' ∣ cs' ⇓ c'
    → σ /ᴺ `rec n cz cs ⇓ c'

  `sub-app-lam : ∀{A B}
    {f : Neut wh Γ (A `→ B)}
    {a : Val wh Γ A}
    {f' : Bind wh Φ A B}
    {a' : Val wh Φ A}
    {b' : Val wh Φ B}
    (pf : σ /ᴺ f ⇓ `λ f')
    (pa : σ / a ⇓ a')
    (pb : f' // a' ⇓ b')
    → σ /ᴺ f `∙ a ⇓ b'

  `sub-app-neut : ∀{A B}
    {f : Neut wh Γ (A `→ B)}
    {a : Val wh Γ A}
    {f' : Neut wh Φ (A `→ B)}
    {a' : Val wh Φ A}
    (pf : σ /ᴺ f ⇓ `neut f')
    (pa : σ / a ⇓ a')
    → σ /ᴺ f `∙ a ⇓ `neut (f' `∙ a')

----------------------------------------------------------------------

_/⇓_ : ∀{Γ Δ A}
  (σ : Env Δ Γ)
  (a : Val wh Γ A)
  → Set
σ /⇓ a = ∃ λ a' → σ / a ⇓ a'

_/ᴮ⇓_ : ∀{Γ Δ A B}
  (σ : Env Δ Γ)
  (f : Bind wh Γ A B)
  → Set
σ /ᴮ⇓ f = ∃ λ f' → σ /ᴮ f ⇓ f'

----------------------------------------------------------------------

id-renᴿ : ∀{Γ A} (i : Var Γ A) → renᴿ idRen i ≡ i
id-renᴿ here = refl
id-renᴿ (there i) rewrite id-renᴿ i = refl

id-renˢ : ∀{Φ Γ} (σ : Env Φ Γ) → renˢ idRen σ ≡ σ
id-ren : ∀{m Γ A} (a : Val m Γ A) → ren idRen a ≡ a
id-renᴺ : ∀{m Γ A} (a : Neut m Γ A) → renᴺ idRen a ≡ a
id-renᴮ : ∀{m Γ A B} (f : Bind m Γ A B) → renᴮ idRen f ≡ f

id-renᴮ (`val a) rewrite id-ren a = refl
id-renᴮ (σ `/ a) rewrite id-renˢ σ | id-ren a = refl

id-renˢ ∅ = refl
id-renˢ (σ , a) rewrite id-renˢ σ | id-ren a = refl

id-ren `true = refl
id-ren `false = refl
id-ren `zero = refl
id-ren (`suc n) rewrite id-ren n = refl
id-ren (`λ (`val f)) rewrite id-ren f = refl
id-ren (`λ (σ `/ f)) rewrite id-renˢ σ = refl
id-ren (`neut a) rewrite id-renᴺ a = refl

id-renᴺ (`var i) rewrite id-renᴿ i = refl
id-renᴺ (f `∙ a) rewrite id-renᴺ f | id-ren a = refl
id-renᴺ (`if b then ct else cf)
  rewrite id-renᴺ b | id-ren ct | id-ren cf = refl
id-renᴺ (`rec n cz cs)
  rewrite id-renᴺ n | id-ren cz | id-renᴮ cs = refl

----------------------------------------------------------------------

infix 1 _⟱_
infix 1 _⟱ᴺ_

data _⟱_ {Γ} : ∀{A} (a : Val wh Γ A) (a' : Val nf Γ A) → Set
data _⟱ᴺ_ {Γ} : ∀{A} (a : Neut wh Γ A) (a' : Neut nf Γ A) → Set

data _⟱ᴮ_ {Γ A B} : (f : Bind wh Γ A B) (f' : Bind nf Γ A B) → Set where
  `quote-bind : ∀{Δ}
    {f : Val wh (Δ , A) B}
    {f' : Val wh (Γ , A) B}
    {f'' : Val nf (Γ , A) B}
    {σ : Env Γ Δ}
    → ↑₁ σ / f  ⇓ f'
    → f' ⟱ f''
    → (σ `/ f) ⟱ᴮ (`val f'')

data _⟱_ {Γ} where
  `quote-true : `true ⟱ `true
  `quote-false : `false ⟱ `false
  `quote-zero : `zero ⟱ `zero

  `quote-suc :
    {n : Val wh Γ `ℕ}
    {n' : Val nf Γ `ℕ}
    → n ⟱ n'
    → `suc n ⟱ `suc n'

  `quote-lam : ∀{A B}
    {f : Bind wh Γ A B}
    {f' : Bind nf Γ A B}
    → f ⟱ᴮ f'
    → `λ f ⟱ `λ f'

  `quote-neut : ∀{A} {a : Neut wh Γ A} {a' : Neut nf Γ A}
    → a ⟱ᴺ a'
    → `neut a ⟱ `neut a'

data _⟱ᴺ_ {Γ} where
  `quote-var : ∀{A}
    (i : Var Γ A)
    → `var i ⟱ᴺ `var i

  `quote-if : ∀{C}
    {b : Neut wh Γ `Bool}
    {ct cf : Val wh Γ C}
    {b' : Neut nf Γ `Bool}
    {ct' cf' : Val nf Γ C}
    (pb : b ⟱ᴺ b')
    (pct : ct ⟱ ct')
    (pcf : cf ⟱ cf')
    → `if b then ct else cf ⟱ᴺ `if b' then ct' else cf'

  `quote-rec : ∀{C}
    {n : Neut wh Γ `ℕ}
    {cz : Val wh Γ C}
    {cs : Bind wh Γ C C}
    {n' : Neut nf Γ `ℕ}
    {cz' : Val nf Γ C}
    {cs' : Bind nf Γ C C}
    → n ⟱ᴺ n'
    → cz ⟱ cz'
    → cs ⟱ᴮ cs'
    → `rec n cz cs ⟱ᴺ `rec n' cz' cs'

  `quote-app : ∀{A B}
    {f : Neut wh Γ (A `→ B)}
    {a : Val wh Γ A}
    {f' : Neut nf Γ (A `→ B)}
    {a' : Val nf Γ A}
    (pf : f ⟱ᴺ f')
    (pa : a ⟱ a')
    → f `∙ a ⟱ᴺ f' `∙ a'

----------------------------------------------------------------------

⟦_⊢_∶ʳ_⟧ : (Γ : Ctx) (A : Type) (a : Val wh Γ A) → Set

⟦_⊩_⇒_∶ʳ_⟧ : (Γ : Ctx) (A B : Type) (f : Bind wh Γ A B) → Set
⟦ Γ ⊩ A ⇒ B ∶ʳ σ `/ b ⟧ = ∀{Δ}
  (Δ≥Γ : Ren Δ Γ)
  (a : Val wh Δ A)
  → ⟦ Δ ⊢ A ∶ʳ a ⟧
  → ∃ λ b'
  → renˢ Δ≥Γ σ , a / b ⇓ b'
  ∧ ⟦ Δ ⊢ B ∶ʳ b' ⟧

⟦ Γ ⊢ `Bool ∶ʳ `true ⟧ = ⊤
⟦ Γ ⊢ `Bool ∶ʳ `false ⟧ = ⊤
⟦ Γ ⊢ `Bool ∶ʳ `neut b ⟧ = ∃ λ b' → b ⟱ᴺ b'

⟦ Γ ⊢ `ℕ ∶ʳ `zero ⟧ = ⊤
⟦ Γ ⊢ `ℕ ∶ʳ `suc n ⟧ = ⟦ Γ ⊢ `ℕ ∶ʳ n ⟧
⟦ Γ ⊢ `ℕ ∶ʳ `neut n ⟧ = ∃ λ n' → n ⟱ᴺ n'

⟦ Γ ⊢ (A `→ B) ∶ʳ `λ f ⟧ = ⟦ Γ ⊩ A ⇒ B ∶ʳ f ⟧
⟦ Γ ⊢ (A `→ B) ∶ʳ `neut f ⟧ = ∃ λ f' → f ⟱ᴺ f'

Val-Model = ⟦_⊢_∶ʳ_⟧
syntax Val-Model Γ A a = ⟦ Γ ⊢ a ∶ A ⟧

Bind-Model = ⟦_⊩_⇒_∶ʳ_⟧
syntax Bind-Model Γ A B f = ⟦ Γ ⊩ f ∶ A ⇒ B ⟧

----------------------------------------------------------------------

⟦_⊢_∶ʳ_/_∶ʳ_⟧ : (Φ Γ : Ctx) (σ : Env Φ Γ) (A : Type) (a : Val wh Γ A) → Set
⟦ Φ ⊢ Γ ∶ʳ σ / A ∶ʳ a ⟧ = ∃ λ a' → σ / a ⇓ a' ∧ ⟦ Φ ⊢ a' ∶ A ⟧

HSub-Model = ⟦_⊢_∶ʳ_/_∶ʳ_⟧
syntax HSub-Model Φ Γ σ A a = ⟦ Φ ⊢ σ ∶ Γ / a ∶ A ⟧

----------------------------------------------------------------------

⟦_⊩_∶ʳ_/_⇒_∶ʳ_⟧ : (Φ Γ : Ctx) (σ : Env Φ Γ) (A B : Type) (a : Bind wh Γ A B) → Set
⟦ Φ ⊩ Γ ∶ʳ σ / A ⇒ B ∶ʳ f ⟧ = ∃ λ f' → σ /ᴮ f ⇓ f' ∧ ⟦ Φ ⊩ f' ∶ A ⇒ B ⟧

BSub-Model = ⟦_⊩_∶ʳ_/_⇒_∶ʳ_⟧
syntax BSub-Model Φ Γ σ A B f = ⟦ Φ ⊩ σ ∶ Γ / f ∶ A ⇒ B ⟧

----------------------------------------------------------------------

data ⟦_⊨_∶ʳ_⟧ (Φ : Ctx) : (Γ : Ctx) (σ : Env Φ Γ) → Set where
  ∅ : ⟦ Φ ⊨ ∅ ∶ʳ ∅ ⟧
  _,_ : ∀{Γ A} {σ : Env Φ Γ} {a : Val wh Φ A}
    → ⟦ Φ ⊨ Γ ∶ʳ σ ⟧
    → ⟦ Φ ⊢ a ∶ A ⟧
    → ⟦ Φ ⊨ Γ , A ∶ʳ σ , a ⟧

Env-Model = ⟦_⊨_∶ʳ_⟧
syntax Env-Model Φ Γ σ = ⟦ Φ ⊨ σ ∶ Γ ⟧

⟦lookup⟧ : ∀{Φ Γ A} {σ : Env Φ Γ}
  (⟦σ⟧ : ⟦ Φ ⊨ σ ∶ Γ ⟧) (i : Var Γ A)
  → ⟦ Φ ⊢ lookup σ i ∶ A ⟧
⟦lookup⟧ (⟦σ⟧ , ⟦a⟧) here = ⟦a⟧
⟦lookup⟧ (⟦σ⟧ , _) (there i) = ⟦lookup⟧ ⟦σ⟧ i

----------------------------------------------------------------------

comp : ∀{Γ Φ Δ}
  (Δ≥Φ : Ren Δ Φ)
  (Φ≥Γ : Ren Φ Γ)
  → Ren Δ Γ
comp done Φ≥Γ = Φ≥Γ
comp (skip Δ≥Φ) Φ≥Γ = skip (comp Δ≥Φ Φ≥Γ)
comp (keep Δ≥Φ) (skip Φ≥Γ) = skip (comp Δ≥Φ Φ≥Γ)
comp (keep Δ≥Φ) (keep Φ≥Γ) = keep (comp Δ≥Φ Φ≥Γ)

comp-renᴿ : ∀{Γ Φ Δ A}
  (Δ≥Φ : Ren Δ Φ)
  (Φ≥Γ : Ren Φ Γ)
  (i : Var Γ A)
  → renᴿ Δ≥Φ (renᴿ Φ≥Γ i) ≡ renᴿ (comp Δ≥Φ Φ≥Γ) i
comp-renᴿ done done ()
comp-renᴿ (skip Δ≥Φ) Φ≥Γ i = cong there (comp-renᴿ Δ≥Φ Φ≥Γ i)
comp-renᴿ (keep Δ≥Φ) (skip Φ≥Γ) i = comp-renᴿ (skip Δ≥Φ) Φ≥Γ i
comp-renᴿ (keep Δ≥Φ) (keep Φ≥Γ) here = refl
comp-renᴿ (keep Δ≥Φ) (keep Φ≥Γ) (there i) = comp-renᴿ (skip Δ≥Φ) Φ≥Γ i

----------------------------------------------------------------------

comp-ren : ∀{Γ Φ Δ A}
  (Δ≥Φ : Ren Δ Φ)
  (Φ≥Γ : Ren Φ Γ)
  (a : Val wh Γ A)
  → ren Δ≥Φ (ren Φ≥Γ a) ≡ ren (comp Δ≥Φ Φ≥Γ) a

comp-renᴺ : ∀{Γ Φ Δ A}
  (Δ≥Φ : Ren Δ Φ)
  (Φ≥Γ : Ren Φ Γ)
  (a : Neut wh Γ A)
  → renᴺ Δ≥Φ (renᴺ Φ≥Γ a) ≡ renᴺ (comp Δ≥Φ Φ≥Γ) a

comp-renˢ : ∀{Γ Φ Δ Ω}
  (Ω≥Δ : Ren Ω Δ)
  (Δ≥Φ : Ren Δ Φ)
  (σ : Env Φ Γ)
  → renˢ Ω≥Δ (renˢ Δ≥Φ σ) ≡ renˢ (comp Ω≥Δ Δ≥Φ) σ
comp-renˢ Δ≥Φ Φ≥Γ ∅ = refl
comp-renˢ Δ≥Φ Φ≥Γ (σ , a)
  rewrite comp-renˢ Δ≥Φ Φ≥Γ σ | comp-ren Δ≥Φ Φ≥Γ a = refl

comp-renᴮ : ∀{Γ Φ Δ A B}
  (Δ≥Φ : Ren Δ Φ)
  (Φ≥Γ : Ren Φ Γ)
  (f : Bind wh Γ A B)
  → renᴮ Δ≥Φ (renᴮ Φ≥Γ f) ≡ renᴮ (comp Δ≥Φ Φ≥Γ) f
comp-renᴮ Δ≥Φ Φ≥Γ (σ `/ b) rewrite comp-renˢ Δ≥Φ Φ≥Γ σ = refl

comp-ren Δ≥Φ Φ≥Γ `true = refl
comp-ren Δ≥Φ Φ≥Γ `false = refl
comp-ren Δ≥Φ Φ≥Γ `zero = refl
comp-ren Δ≥Φ Φ≥Γ (`suc n) rewrite comp-ren Δ≥Φ Φ≥Γ n = refl
comp-ren Δ≥Φ Φ≥Γ (`λ f) rewrite comp-renᴮ Δ≥Φ Φ≥Γ f = refl
comp-ren Δ≥Φ Φ≥Γ (`neut a) rewrite comp-renᴺ Δ≥Φ Φ≥Γ a = refl

comp-renᴺ Δ≥Φ Φ≥Γ (`var i) rewrite comp-renᴿ Δ≥Φ Φ≥Γ i = refl
comp-renᴺ Δ≥Φ Φ≥Γ (f `∙ a)
  rewrite comp-renᴺ Δ≥Φ Φ≥Γ f | comp-ren Δ≥Φ Φ≥Γ a = refl
comp-renᴺ Δ≥Φ Φ≥Γ (`if b then ct else cf)
  rewrite comp-renᴺ Δ≥Φ Φ≥Γ b | comp-ren Δ≥Φ Φ≥Γ ct | comp-ren Δ≥Φ Φ≥Γ cf = refl
comp-renᴺ Δ≥Φ Φ≥Γ (`rec n cz cs)
  rewrite comp-renᴺ Δ≥Φ Φ≥Γ n | comp-ren Δ≥Φ Φ≥Γ cz | comp-renᴮ Δ≥Φ Φ≥Γ cs = refl

----------------------------------------------------------------------

comp-id : ∀{Φ Γ} (Φ≥Γ : Ren Φ Γ)
  → comp idRen Φ≥Γ ≡ comp Φ≥Γ idRen
comp-id done = refl
comp-id (skip x) = cong skip (comp-id x)
comp-id (keep x) = cong keep (comp-id x)

----------------------------------------------------------------------

renˢ-comp : ∀{Δ Φ Γ} B (σ : Env Φ Γ) (Δ≥Φ : Ren Δ Φ)
  → renˢ (skip {A = B} idRen) (renˢ Δ≥Φ σ) ≡ renˢ (keep Δ≥Φ) (renˢ (skip idRen) σ)
renˢ-comp B σ Δ≥Φ
  rewrite comp-renˢ (wknRen₁ {A = B}) Δ≥Φ σ | comp-renˢ (keep Δ≥Φ) (wknRen₁ {A = B}) σ | comp-id Δ≥Φ
  = refl

----------------------------------------------------------------------

lookup-renˢ : ∀{Φ Γ Δ A}
  (σ : Env Φ Γ)
  (Δ≥Φ : Ren Δ Φ)
  (i : Var Γ A)
  (a : Val wh Φ A)
  → a ≡ lookup σ i
  → ren Δ≥Φ a ≡ lookup (renˢ Δ≥Φ σ) i
lookup-renˢ (σ , a) Δ≥Φ here a' q = cong (ren Δ≥Φ) q
lookup-renˢ (σ , a) Δ≥Φ (there i) a' q = lookup-renˢ σ Δ≥Φ i a' q

----------------------------------------------------------------------

ren-hsub : ∀{Φ Δ Γ A} {a : Val wh Γ A} {a' : Val wh Φ A} {σ : Env Φ Γ}
  (Δ≥Φ : Ren Δ Φ) → σ / a ⇓ a' → renˢ Δ≥Φ σ / a ⇓ ren Δ≥Φ a'
renᴺ-hsub : ∀{Φ Δ Γ A} {a : Neut wh Γ A} {a' : Val wh Φ A} {σ : Env Φ Γ}
  (Δ≥Φ : Ren Δ Φ) → σ /ᴺ a ⇓ a' → renˢ Δ≥Φ σ /ᴺ a ⇓ ren Δ≥Φ a'

renˢ-hsub : ∀{Φ Ψ Γ Δ} {ρ : Env Ψ Γ} {ρ' : Env Φ Γ} {σ : Env Φ Ψ}
  (Δ≥Φ : Ren Δ Φ) → σ ∘ ρ ⇓ ρ' → renˢ Δ≥Φ σ ∘ ρ ⇓ renˢ Δ≥Φ ρ'
renˢ-hsub Δ≥Φ `comp-emp = `comp-emp
renˢ-hsub Δ≥Φ (`comp-ext ρ⇓ρ' a⇓a') = `comp-ext (renˢ-hsub Δ≥Φ ρ⇓ρ') (ren-hsub Δ≥Φ a⇓a')

renᴮ-hsub : ∀{Φ Δ Γ A B} {f : Bind wh Γ A B} {f' : Bind wh Φ A B} {σ : Env Φ Γ}
  (Δ≥Φ : Ren Δ Φ) → σ /ᴮ f ⇓ f' → renˢ Δ≥Φ σ /ᴮ f ⇓ renᴮ Δ≥Φ f'
renᴮ-hsub Δ≥Φ (`sub-bind ρ∘ρ') = `sub-bind (renˢ-hsub Δ≥Φ ρ∘ρ')

ren-bsub : ∀{Δ Γ A B} {f : Bind wh Γ A B} {a : Val wh Γ A} {b : Val wh Γ B}
  (Δ≥Γ : Ren Δ Γ) → f // a ⇓ b → renᴮ Δ≥Γ f // ren Δ≥Γ a ⇓ ren Δ≥Γ b
ren-bsub Δ≥Γ (`app-bind b⇓b') = `app-bind (ren-hsub Δ≥Γ b⇓b')

ren-rec : ∀{Δ Γ C} {n : Val wh Γ `ℕ} {cz : Val wh Γ C} {cs : Bind wh Γ C C} {c : Val wh Γ C}
  (Δ≥Γ : Ren Δ Γ) → rec n of cz ∣ cs ⇓ c → rec (ren Δ≥Γ n) of (ren Δ≥Γ cz) ∣ (renᴮ Δ≥Γ cs) ⇓ ren Δ≥Γ c
ren-rec Δ≥Γ `rec-zero = `rec-zero
ren-rec Δ≥Γ (`rec-suc p c⇓c') = `rec-suc (ren-rec Δ≥Γ p) (ren-bsub Δ≥Γ c⇓c')
ren-rec Δ≥Γ `rec-neut = `rec-neut

----------------------------------------------------------------------

ren-hsub Δ≥Φ `sub-true = `sub-true
ren-hsub Δ≥Φ `sub-false = `sub-false
ren-hsub Δ≥Φ `sub-zero = `sub-zero
ren-hsub Δ≥Φ (`sub-suc n) = `sub-suc (ren-hsub Δ≥Φ n)
ren-hsub Δ≥Φ (`sub-lam f⇓f') = `sub-lam (renᴮ-hsub Δ≥Φ f⇓f')
ren-hsub Δ≥Φ (`sub-neut a⇓a') = `sub-neut (renᴺ-hsub Δ≥Φ a⇓a')

renᴺ-hsub {σ = σ} Δ≥Φ (`sub-var i)
  rewrite lookup-renˢ σ Δ≥Φ i (lookup σ i) refl = `sub-var i
renᴺ-hsub Δ≥Φ (`sub-if-true b⇓b' ct⇓ct')
  = `sub-if-true (renᴺ-hsub Δ≥Φ b⇓b') (ren-hsub Δ≥Φ ct⇓ct')
renᴺ-hsub Δ≥Φ (`sub-if-false b⇓b' cf⇓cf')
  = `sub-if-false (renᴺ-hsub Δ≥Φ b⇓b') (ren-hsub Δ≥Φ cf⇓cf')
renᴺ-hsub Δ≥Φ (`sub-if-neut b⇓b' ct⇓ct' cf⇓cf')
  = `sub-if-neut (renᴺ-hsub Δ≥Φ b⇓b') (ren-hsub Δ≥Φ ct⇓ct') (ren-hsub Δ≥Φ cf⇓cf')
renᴺ-hsub Δ≥Φ (`sub-app-lam f⇓f' a⇓a' b⇓b')
  = `sub-app-lam (renᴺ-hsub Δ≥Φ f⇓f') (ren-hsub Δ≥Φ a⇓a') (ren-bsub Δ≥Φ b⇓b')
renᴺ-hsub Δ≥Φ (`sub-app-neut f⇓f' a⇓a')
  = `sub-app-neut (renᴺ-hsub Δ≥Φ f⇓f') (ren-hsub Δ≥Φ a⇓a')
renᴺ-hsub Δ≥Φ (`sub-rec n⇓n' cz⇓cz' cs⇓cs' p)
  = `sub-rec (renᴺ-hsub Δ≥Φ n⇓n') (ren-hsub Δ≥Φ cz⇓cz') (renᴮ-hsub Δ≥Φ cs⇓cs') (ren-rec Δ≥Φ p)

----------------------------------------------------------------------

ren-quote : ∀{Δ Γ A} {a : Val wh Γ A} {a' : Val nf Γ A} (Δ≥Γ : Ren Δ Γ) → a ⟱ a' → ren Δ≥Γ a ⟱ ren Δ≥Γ a'
ren-quoteᴺ : ∀{Δ Γ A} {a : Neut wh Γ A} {a' : Neut nf Γ A} (Δ≥Γ : Ren Δ Γ) → a ⟱ᴺ a' → renᴺ Δ≥Γ a ⟱ᴺ renᴺ Δ≥Γ a'

ren-quoteᴮ : ∀{Δ Γ A B} {f : Bind wh Γ A B} {f' : Bind nf Γ A B} (Δ≥Γ : Ren Δ Γ)
  → f ⟱ᴮ f' → renᴮ Δ≥Γ f ⟱ᴮ renᴮ Δ≥Γ f'
ren-quoteᴮ {A = A} Δ≥Γ (`quote-bind {σ = σ} f⇓f' f'⟱f'')
  with ren-hsub (keep Δ≥Γ) f⇓f'
... | ih₁
  with ren-quote (keep Δ≥Γ) f'⟱f''
... | ih₂
  rewrite sym (renˢ-comp A σ Δ≥Γ)
  = `quote-bind ih₁ ih₂

----------------------------------------------------------------------

ren-quote Δ≥Γ `quote-true = `quote-true
ren-quote Δ≥Γ `quote-false = `quote-false
ren-quote Δ≥Γ `quote-zero = `quote-zero
ren-quote Δ≥Γ (`quote-suc n⟱n') = `quote-suc (ren-quote Δ≥Γ n⟱n')
ren-quote Δ≥Γ (`quote-lam f⟱f') = `quote-lam (ren-quoteᴮ Δ≥Γ f⟱f')
ren-quote Δ≥Γ (`quote-neut a⟱a') = `quote-neut (ren-quoteᴺ Δ≥Γ a⟱a')

ren-quoteᴺ Δ≥Γ (`quote-var i) = `quote-var (renᴿ Δ≥Γ i)
ren-quoteᴺ Δ≥Γ (`quote-if b⟱b' ct⟱ct' cf⟱cf')
  = `quote-if (ren-quoteᴺ Δ≥Γ b⟱b') (ren-quote Δ≥Γ ct⟱ct') (ren-quote Δ≥Γ cf⟱cf')
ren-quoteᴺ Δ≥Γ (`quote-app f⟱f' a⟱a')
  = `quote-app (ren-quoteᴺ Δ≥Γ f⟱f') (ren-quote Δ≥Γ a⟱a')

ren-quoteᴺ Δ≥Γ (`quote-rec n⟱n' cz⟱cz' cs⟱cs')
  = `quote-rec (ren-quoteᴺ Δ≥Γ n⟱n') (ren-quote Δ≥Γ cz⟱cz') (ren-quoteᴮ Δ≥Γ cs⟱cs')

----------------------------------------------------------------------

reflect : ∀{Γ} A
  (a : Neut wh Γ A)
  {a' : Neut nf Γ A}
  (a⟱a' : a ⟱ᴺ a')
  → ⟦ Γ ⊢ `neut a ∶ A ⟧
reflect `Bool b b⟱b' = _ , b⟱b'
reflect `ℕ n n⟱n' = _ , n⟱n'
reflect (A `→ B) f f⟱f' = _ , f⟱f'

reflectᴿ : ∀{Γ} A
  (i : Var Γ A)
  → ⟦ Γ ⊢ `neut (`var i) ∶ A ⟧
reflectᴿ A i = reflect A (`var i) (`quote-var i)

----------------------------------------------------------------------

reify : ∀{Γ} A
  (a : Val wh Γ A)
  (⟦a⟧ : ⟦ Γ ⊢ a ∶ A ⟧)
  → ∃ λ a'
  → a ⟱ a'

reify `Bool `true tt = `true , `quote-true
reify `Bool `false tt = `false , `quote-false
reify `Bool (`neut b) (b' , b⟱b') = `neut b' , `quote-neut b⟱b'
reify `ℕ `zero tt = `zero , `quote-zero
reify `ℕ (`suc n) ⟦n⟧
  with reify `ℕ n ⟦n⟧
... | n' , n⟱n'
  = `suc n' , `quote-suc n⟱n'
reify `ℕ (`neut n) (n' , n⟱n') = `neut n' , `quote-neut n⟱n'
reify (A `→ B) (`neut f) (f' , f⟱f') = `neut f' , `quote-neut f⟱f'

reify (A `→ B) (`λ (σ `/ b)) ⟦f⟧
  with ⟦f⟧ (skip idRen) `x (reflect A `xᴺ (`quote-var here))
... | b' , b⇓b' , ⟦b⟧
  with reify B _ ⟦b⟧
... | b'' , b'⟱b''
  = `λ (`val b'') , `quote-lam (`quote-bind b⇓b' b'⟱b'')

----------------------------------------------------------------------

_⟦∙⟧_ : ∀{Φ Γ A B σ f a}
  → ⟦ Φ ⊢ σ ∶ Γ / `neut f ∶ A `→ B ⟧
  → ⟦ Φ ⊢ σ ∶ Γ / a ∶ A ⟧
  → ⟦ Φ ⊢ σ ∶ Γ / `neut (f `∙ a) ∶ B ⟧

(`neut f' , `sub-neut f⇓f' , f'' , f'⟱f'') ⟦∙⟧ (a' , a⇓a' , ⟦a⟧)
  with reify _ a' ⟦a⟧
... | a'' , a'⟱a''
  = `neut (f' `∙ a')
  , `sub-neut (`sub-app-neut f⇓f' a⇓a')
  , reflect _ (f' `∙ a') (`quote-app f'⟱f'' a'⟱a'')

(`λ (ρ `/ b) , `sub-neut f⇓λb , ⟦f⟧) ⟦∙⟧ (a' , a⇓a' , ⟦a⟧)
  with ⟦f⟧ idRen a' ⟦a⟧
... | b' , b⇓b' , ⟦b⟧
  rewrite id-renˢ ρ
  = b' , `sub-neut (`sub-app-lam f⇓λb a⇓a' (`app-bind b⇓b')) , ⟦b⟧

----------------------------------------------------------------------

⟦if⟧_⟦then⟧_⟦else⟧_ : ∀{Φ Γ C σ b ct cf}
  → ⟦ Φ ⊢ σ ∶ Γ / `neut b ∶ `Bool ⟧
  → ⟦ Φ ⊢ σ ∶ Γ / ct ∶ C ⟧
  → ⟦ Φ ⊢ σ ∶ Γ / cf ∶ C ⟧
  → ⟦ Φ ⊢ σ ∶ Γ / `neut (`if b then ct else cf) ∶ C ⟧

⟦if⟧ (`true , `sub-neut b⇓true , tt) ⟦then⟧ (ct' , ct⇓ct' , ⟦ct⟧) ⟦else⟧ _
  = ct' , `sub-neut (`sub-if-true b⇓true ct⇓ct') , ⟦ct⟧
⟦if⟧ (`false , `sub-neut b⇓false , tt) ⟦then⟧ _ ⟦else⟧ (cf' , cf⇓cf' , ⟦cf⟧)
  = cf' , `sub-neut (`sub-if-false b⇓false cf⇓cf') , ⟦cf⟧
⟦if⟧ (`neut b' , `sub-neut b⇓b' , b'' , b'⟱b'') ⟦then⟧ (ct' , ct⇓ct' , ⟦ct⟧) ⟦else⟧ (cf' , cf⇓cf' , ⟦cf⟧)
  with reify _ ct' ⟦ct⟧
... | ct'' , ct'⟱ct''
  with reify _ cf' ⟦cf⟧
... | cf'' , cf'⟱cf''
  = `neut (`if b' then ct' else cf')
  , `sub-neut (`sub-if-neut b⇓b' ct⇓ct' cf⇓cf')
  , reflect _ (`if b' then ct' else cf') (`quote-if b'⟱b'' ct'⟱ct'' cf'⟱cf'')

----------------------------------------------------------------------

⟦rec⟧' : ∀{Γ C} n cz cs
  → ⟦ Γ ⊢ n ∶ `ℕ ⟧
  → ⟦ Γ ⊢ cz ∶ C ⟧
  → ⟦ Γ ⊩ cs ∶ C ⇒ C ⟧
  → ∃ λ c
  → rec n of cz ∣ cs ⇓ c
  ∧ ⟦ Γ ⊢ c ∶ C ⟧

⟦rec⟧' `zero cz cs tt ⟦cz⟧ ⟦cs⟧
  = cz , `rec-zero , ⟦cz⟧

⟦rec⟧' (`suc n) cz (σ `/ cs) ⟦n⟧ ⟦cz⟧ ⟦cs⟧
  with ⟦rec⟧' n cz (σ `/ cs) ⟦n⟧ ⟦cz⟧ ⟦cs⟧
... | c , rec⇓c , ⟦c⟧
  with ⟦cs⟧ idRen  c ⟦c⟧
... | c' , c⇓c' , ⟦c'⟧
  rewrite id-renˢ σ
  = c' , `rec-suc rec⇓c (`app-bind c⇓c') , ⟦c'⟧

⟦rec⟧' {C = C} (`neut n) cz (σ `/ cs) (n' , n⟱n') ⟦cz⟧ ⟦cs⟧
  with reify C cz ⟦cz⟧
... | cz' , cz⟱cz'
  with ⟦cs⟧ (skip idRen) `x (reflect C `xᴺ (`quote-var here))
... | c , cs⇓c , ⟦c⟧
  with reify C c ⟦c⟧
... | c' , c⟱c'
  = `neut (`rec n cz (σ `/ cs))
  , `rec-neut
  , reflect C (`rec n cz (σ `/ cs)) (`quote-rec n⟱n' cz⟱cz' (`quote-bind cs⇓c c⟱c'))

----------------------------------------------------------------------

⟦rec⟧ : ∀{Φ Γ C σ n cz cs}
  → ⟦ Φ ⊢ σ ∶ Γ / `neut n ∶ `ℕ ⟧
  → ⟦ Φ ⊢ σ ∶ Γ / cz ∶ C ⟧
  → ⟦ Φ ⊩ σ ∶ Γ / cs ∶ C ⇒ C ⟧
  → ⟦ Φ ⊢ σ ∶ Γ / `neut (`rec n cz cs) ∶ C ⟧
⟦rec⟧ (n' , `sub-neut n⇓n' , ⟦n⟧) (cz' , cz⇓cz' , ⟦cz⟧) (cs' , cs⇓cs' , ⟦cs⟧)
  with ⟦rec⟧' n' cz' cs' ⟦n⟧ ⟦cz⟧ ⟦cs⟧
... | c , rec⇓c , ⟦c⟧
  = c
  , `sub-neut (`sub-rec n⇓n' cz⇓cz' cs⇓cs' rec⇓c)
  , ⟦c⟧

----------------------------------------------------------------------

mono : ∀{Γ Δ} (Δ≥Γ : Ren Δ Γ)
  A (a : Val wh Γ A)
  (⟦a⟧ : ⟦ Γ ⊢ a ∶ A ⟧)
  → ⟦ Δ ⊢ ren Δ≥Γ a ∶ A ⟧

mono Δ≥Γ `Bool `true tt = tt
mono Δ≥Γ `Bool `false tt = tt
mono Δ≥Γ `Bool (`neut b) (b' , b⟱b') = renᴺ Δ≥Γ b' , ren-quoteᴺ Δ≥Γ b⟱b'
mono Δ≥Γ `ℕ `zero tt = tt
mono Δ≥Γ `ℕ (`suc n) ⟦n⟧ = mono Δ≥Γ `ℕ n ⟦n⟧
mono Δ≥Γ `ℕ (`neut n) (n' , n⟱n') = renᴺ Δ≥Γ n' , ren-quoteᴺ Δ≥Γ n⟱n'
mono Δ≥Γ (A `→ B) (`neut f) (f' , f⟱f') = renᴺ Δ≥Γ f' , ren-quoteᴺ Δ≥Γ f⟱f'

mono Δ≥Γ (A `→ B) (`λ (σ `/ f)) ⟦λf⟧ = result where
  result : ⟦ _ ⊢ ren Δ≥Γ (`λ (σ `/ f)) ∶ A `→ B ⟧
  result Ω≥Δ a ⟦a⟧
    rewrite comp-renˢ Ω≥Δ Δ≥Γ σ
    = ⟦λf⟧ (comp Ω≥Δ Δ≥Γ) a ⟦a⟧

----------------------------------------------------------------------

monos : ∀{Φ Γ Δ}
  (Δ≥Φ : Ren Δ Φ)
  {σ : Env Φ Γ}
  (⟦σ⟧ : ⟦ Φ ⊨ σ ∶ Γ ⟧)
  → ⟦ Δ ⊨ renˢ Δ≥Φ σ ∶ Γ ⟧

monos Δ≥Φ ∅ = ∅
monos Δ≥Φ (_,_ {A = A} ⟦σ⟧ ⟦a⟧) = monos Δ≥Φ ⟦σ⟧ , mono Δ≥Φ A _ ⟦a⟧

----------------------------------------------------------------------

⟦hsub⟧ : ∀{Φ Γ A}
  {σ : Env Φ Γ}
  (⟦σ⟧ : ⟦ Φ ⊨ σ ∶ Γ ⟧)
  (a : Val wh Γ A)
  → ⟦ Φ ⊢ σ ∶ Γ / a ∶ A ⟧

⟦hsubᴺ⟧ : ∀{Φ Γ A}
  {σ : Env Φ Γ}
  (⟦σ⟧ : ⟦ Φ ⊨ σ ∶ Γ ⟧)
  (a : Neut wh Γ A)
  → ⟦ Φ ⊢ σ ∶ Γ / `neut a ∶ A ⟧

⟦comp⟧ : ∀{Φ Δ Γ}
  {σ : Env Φ Δ}
  (⟦σ⟧ : ⟦ Φ ⊨ σ ∶ Δ ⟧)
  (ρ : Env Δ Γ)
  → ∃ λ ρ'
  → σ ∘ ρ ⇓ ρ'
  ∧ ⟦ Φ ⊨ ρ' ∶ Γ ⟧
⟦comp⟧ ⟦σ⟧ ∅ = ∅ , `comp-emp , ∅
⟦comp⟧ ⟦σ⟧ (ρ , a)
  with ⟦comp⟧ ⟦σ⟧ ρ
... | ρ' , ρ⇓ρ' , ⟦ρ⟧
  with ⟦hsub⟧ ⟦σ⟧ a
... | a' , a⇓a' , ⟦a⟧
  = (ρ' , a') , (`comp-ext ρ⇓ρ' a⇓a') , (⟦ρ⟧ , ⟦a⟧)

⟦hsubᴮ⟧ : ∀{Φ Γ A B}
  {σ : Env Φ Γ}
  (⟦σ⟧ : ⟦ Φ ⊨ σ ∶ Γ ⟧)
  (f : Bind wh Γ A B)
  → ⟦ Φ ⊩ σ ∶ Γ / f ∶ A ⇒ B ⟧
⟦hsubᴮ⟧ ⟦σ⟧ (ρ `/ b)
  with ⟦comp⟧ ⟦σ⟧ ρ
... | ρ' , ρ⇓ρ' , ⟦ρ⟧
  = (ρ' `/ b) , `sub-bind ρ⇓ρ' , (λ Δ≥Φ a ⟦a⟧ → ⟦hsub⟧ (monos Δ≥Φ ⟦ρ⟧ , ⟦a⟧) b)

----------------------------------------------------------------------

⟦hsub⟧ ⟦σ⟧ `true = `true , `sub-true , tt
⟦hsub⟧ ⟦σ⟧ `false = `false , `sub-false , tt
⟦hsub⟧ ⟦σ⟧ `zero = `zero , `sub-zero , tt
⟦hsub⟧ ⟦σ⟧ (`suc n)
  with ⟦hsub⟧ ⟦σ⟧ n
... | n' , n⇓n' , ⟦n⟧
  = `suc n' , `sub-suc n⇓n' , ⟦n⟧

⟦hsub⟧ ⟦σ⟧ (`λ f)
  with ⟦hsubᴮ⟧ ⟦σ⟧ f
... | f' , f⇓f' , ⟦f⟧
  = `λ f' , `sub-lam f⇓f' , ⟦f⟧

⟦hsub⟧ ⟦σ⟧ (`neut a) = ⟦hsubᴺ⟧ ⟦σ⟧ a
⟦hsubᴺ⟧ {σ = σ} ⟦σ⟧ (`var i) = lookup σ i , (`sub-neut (`sub-var i)) , ⟦lookup⟧ ⟦σ⟧ i
⟦hsubᴺ⟧ ⟦σ⟧ (f `∙ a) = ⟦hsubᴺ⟧ ⟦σ⟧ f ⟦∙⟧ ⟦hsub⟧ ⟦σ⟧ a
⟦hsubᴺ⟧ ⟦σ⟧ (`if b then ct else cf) = ⟦if⟧ ⟦hsubᴺ⟧ ⟦σ⟧ b ⟦then⟧ ⟦hsub⟧ ⟦σ⟧ ct ⟦else⟧ ⟦hsub⟧ ⟦σ⟧ cf
⟦hsubᴺ⟧ ⟦σ⟧ (`rec n cz cs) = ⟦rec⟧ (⟦hsubᴺ⟧ ⟦σ⟧ n) (⟦hsub⟧ ⟦σ⟧ cz) (⟦hsubᴮ⟧ ⟦σ⟧ cs)

----------------------------------------------------------------------

⟦idEnv⟧ : ∀{Γ} → ⟦ Γ ⊨ idEnv ∶ Γ ⟧
⟦idEnv⟧ {∅} = ∅
⟦idEnv⟧ {Γ , A}
  with ⟦idEnv⟧ {Γ}
... | ⟦σ⟧
  = monos wknRen₁ ⟦σ⟧ , reflectᴿ A here

----------------------------------------------------------------------

id-lookup : ∀{Γ A} (i : Var Γ A) → `neut (`var i) ≡ lookup idEnv i
id-lookup here = refl
id-lookup (there i)
  with lookup-renˢ idEnv wknRen₁ i (`neut (`var i)) (id-lookup i)
... | q rewrite id-renᴿ i = q

id-hsub : ∀{Γ A} {a a' : Val wh Γ A} → idEnv / a ⇓ a' → a ≡ a'
id-hsubᴺ : ∀{Γ A} {a : Neut wh Γ A} {a' : Val wh Γ A} → idEnv /ᴺ a ⇓ a' → `neut a ≡ a'

id-comp : ∀{Γ Δ} {ρ ρ' : Env Γ Δ} → idEnv ∘ ρ ⇓ ρ' → ρ ≡ ρ'
id-comp `comp-emp = refl
id-comp (`comp-ext ρ⇓ρ' a⇓a') = cong₂ _,_ (id-comp ρ⇓ρ') (id-hsub a⇓a')

id-hsubᴮ : ∀{Γ A B} {f : Bind wh Γ A B} {f' : Bind wh Γ A B} → idEnv /ᴮ f ⇓ f' → f ≡ f'
id-hsubᴮ (`sub-bind ρ⇓ρ') rewrite id-comp ρ⇓ρ' = refl

----------------------------------------------------------------------

id-hsub `sub-true = refl
id-hsub `sub-false = refl
id-hsub `sub-zero = refl
id-hsub (`sub-suc n⇓n') rewrite id-hsub n⇓n' = refl
id-hsub (`sub-lam f⇓f') rewrite id-hsubᴮ f⇓f' = refl
id-hsub (`sub-neut a⇓a') = id-hsubᴺ a⇓a'

id-hsubᴺ (`sub-var i) = id-lookup i
id-hsubᴺ (`sub-if-true b⇓true ct⇓ct')
  with id-hsubᴺ b⇓true
... | ()
id-hsubᴺ (`sub-if-false b⇓false cf⇓cf')
  with id-hsubᴺ b⇓false
... | ()
id-hsubᴺ (`sub-if-neut b⇓b' ct⇓ct' cf⇓cf')
  rewrite inj-neut (id-hsubᴺ b⇓b') | id-hsub ct⇓ct' | id-hsub cf⇓cf'
  = refl
id-hsubᴺ (`sub-app-lam f⇓λb a⇓a' b⇓b')
  with id-hsubᴺ f⇓λb
... | ()
id-hsubᴺ (`sub-app-neut f⇓f' a⇓a')
  rewrite inj-neut (id-hsubᴺ f⇓f') | id-hsub a⇓a'
  = refl

id-hsubᴺ (`sub-rec n⇓zero cz⇓cz' cs⇓cs' `rec-zero)
  with id-hsubᴺ n⇓zero
... | ()
id-hsubᴺ (`sub-rec n⇓suc cz⇓cz' cs⇓cs' (`rec-suc rec⇓c c⇓c'))
  with id-hsubᴺ n⇓suc
... | ()
id-hsubᴺ (`sub-rec n⇓n' cz⇓cz' cs⇓cs' `rec-neut)
  rewrite inj-neut (id-hsubᴺ n⇓n') | id-hsub cz⇓cz' | id-hsubᴮ cs⇓cs'
  = refl

----------------------------------------------------------------------

reflects : ∀{Φ Γ}
  (σ : Env Φ Γ)
  → ⟦ Φ ⊨ σ ∶ Γ ⟧
reflects ∅ = ∅
reflects (σ , a)
  with ⟦hsub⟧ ⟦idEnv⟧ a
... | a' , a⇓a' , ⟦a⟧
  rewrite id-hsub a⇓a' = reflects σ , ⟦a⟧

hsub : ∀{Φ Γ A}
  (σ : Env Φ Γ)
  (a : Val wh Γ A)
  → ∃ λ a'
  → σ / a ⇓ a'
  ∧ ∃ λ a''
  → a' ⟱ a''
hsub σ a with ⟦hsub⟧ (reflects σ) a
... | a' , a⇓a' , ⟦a⟧
  with reify _ a' ⟦a⟧
... | a'' , a'⟱a''
  = a' , a⇓a' , a'' , a'⟱a''

----------------------------------------------------------------------

data Exp : Ctx → Type → Set where
  `λ : ∀{Γ A B} (f : Exp (Γ , A) B) → Exp Γ (A `→ B)
  `var : ∀{Γ A} (i : Var Γ A) → Exp Γ A
  _`∙_ : ∀{Γ A B} (f : Exp Γ (A `→ B)) (a : Exp Γ A) → Exp Γ B

wnorm : ∀{Γ A} → Exp Γ A → Val wh Γ A
wnorm (`λ b) = `λ (idEnv `/ wnorm b)
wnorm (`var i) = `neut (`var i)
wnorm (f `∙ a)
  with wnorm a
... | a'
  with wnorm f
... | `λ (σ `/ b) = proj₁ (hsub (σ , a') b)
... | `neut f' = `neut (f' `∙ a')

eval : ∀{Φ Γ A} → Env Φ Γ → Exp Γ A → Val wh Φ A
eval σ a = proj₁ (⟦hsub⟧ (reflects σ) (wnorm a))

norm : ∀{Γ A} → Exp Γ A → Val nf Γ A
norm a with hsub idEnv (wnorm a)
... | a' , a⇓a' , a'' , a'⟱a'' = a''

----------------------------------------------------------------------