ExplessConv.agda

module ExplessConv where

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

infixr 4 _,_
infixr 0 _∧_

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

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

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

nsym : ∀{ℓ} {A : Set ℓ} {x y : A} → x ≢ y → y ≢ x
nsym f q = f (sym q)

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

infixr 3 _`→_

data Type : Set where
  `ℕ : 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
  `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
  `rec_`of_`else_ : ∀{C} (n : 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)

Wh = Val wh
Nu = Neut wh
Nf = Val nf
Ne = Neut nf
Clos = Bind wh

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

postulate
  eq-dec : ∀{m Γ A} (x y : Val m Γ A) → Dec (x ≡ y)
  eq-decᴷ : ∀{Γ A B} (f g : Clos Γ A B) → Dec (f ≡ g)

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

inj-exte₁ : ∀{Φ Γ A}
  {σ₁ σ₂ : Env Φ Γ}
  {a₁ a₂ : Val wh Φ A}
  → _≡_ {A = Env Φ (Γ , A)} (σ₁ , a₁) (σ₂ , a₂)
  → σ₁ ≡ σ₂
inj-exte₁ refl = refl

inj-exte₂ : ∀{Φ Γ A}
  {σ₁ σ₂ : Env Φ Γ}
  {a₁ a₂ : Val wh Φ A}
  → _≡_ {A = Env Φ (Γ , A)} (σ₁ , a₁) (σ₂ , a₂)
  → a₁ ≡ a₂
inj-exte₂ refl = refl

inj-val : ∀{Γ A B}
  {b₁ b₂ : Val nf (Γ , A) B}
  → `val b₁ ≡ `val b₂
  → b₁ ≡ b₂
inj-val refl = refl

inj-clos₁ :  ∀{Δ Γ₁ Γ₂ A B}
  {σ₁  : Env Δ Γ₁}
  {b₁ : Val wh (Γ₁ , A) B}
  {σ₂  : Env Δ Γ₂}
  {b₂ : Val wh (Γ₂ , A) B}
  → σ₁ `/ b₁ ≡ σ₂ `/ b₂
  → Γ₁ ≡ Γ₂
inj-clos₁ refl = refl

inj-clos₂ :  ∀{Δ Γ A B}
  {σ₁ σ₂  : Env Δ Γ}
  {b₁ b₂ : Val wh (Γ , A) B}
  → σ₁ `/ b₁ ≡ σ₂ `/ b₂
  → σ₁ ≡ σ₂
inj-clos₂ refl = refl

inj-clos₃ :  ∀{Δ Γ A B}
  {σ₁ σ₂  : Env Δ Γ}
  {b₁ b₂ : Val wh (Γ , A) B}
  → σ₁ `/ b₁ ≡ σ₂ `/ b₂
  → b₁ ≡ b₂
inj-clos₃ refl = refl

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

`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 → Wh Φ A
lookup (σ , a) here = a
lookup (σ , a) (there i) = lookup σ i

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

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 : ∀{m Φ Γ A} (σ : Ren Φ Γ) → Val m Γ A → Val m Φ A
renᴺ : ∀{m Φ Γ A} (σ : Ren Φ Γ) → Neut m Γ A → Neut m Φ A

renˢ : ∀{Φ Γ Δ} → Ren Δ Φ → Env Φ Γ → Env Δ Γ
renˢ Δ≥Φ ∅ = ∅
renˢ Δ≥Φ (σ , a) = renˢ Δ≥Φ σ , ren Δ≥Φ a

renᴮ : ∀{m Φ Γ A B} (σ : Ren Φ Γ) → Bind m Γ A B → Bind m Φ A B
renᴮ σ (`val a) = `val (ren (keep σ) a)
renᴮ σ (ρ `/ b) = renˢ σ ρ `/ b

ren σ `zero = `zero
ren σ (`suc n) = `suc (ren σ n)
ren σ (`λ b) = `λ (renᴮ σ b)
ren σ (`neut n) = `neut (renᴺ σ n)

renᴺ σ (`var j) = `var (renᴿ σ j)
renᴺ σ (n `∙ a) = renᴺ σ n `∙ ren σ a
renᴺ σ (`rec n `of cz `else cs) = `rec renᴺ σ n `of ren σ cz `else 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

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

emb : ∀{Γ A} → Nf Γ A → Wh Γ A
embᴺ : ∀{Γ A} → Ne Γ A → Nu Γ A

embᴮ : ∀{Γ A B} → Bind nf Γ A B → Clos Γ A B
embᴮ (`val b) = idEnv `/ emb b

emb `zero = `zero
emb (`suc n) = `suc (emb n)
emb (`λ b) = `λ (embᴮ b)
emb (`neut a) = `neut (embᴺ a)

embᴺ (`var i) = `var i
embᴺ (f `∙ a) = embᴺ f `∙ emb a
embᴺ (`rec n `of cz `else cs) = `rec embᴺ n `of emb cz `else embᴮ cs

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

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

data _/_⇓_ {Φ Γ} (σ : Env Φ Γ) : ∀{A} → Wh Γ A → Wh Φ A → Set
data _/ᴺ_⇓_ {Φ Γ} (σ : Env Φ Γ) : ∀{A} → Nu Γ A → Wh Φ A → Set

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

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

data _∙ᴷ_⇓_ {Γ A B} : Clos Γ A B → Wh Γ A → Wh Γ B → Set where
  `app-clos : ∀{Δ}
    {b : Wh (Δ , A) B}
    {σ : Env Γ Δ}
    {a : Wh Γ A}
    {b' : Wh Γ B}
    → σ , a / b ⇓ b'
    → (σ `/ b) ∙ᴷ a ⇓ b'

data _∙_⇓_ {Γ A B} : Wh Γ (A `→ B) → Wh Γ A → Wh Γ B → Set where
  `app-lam :
    {f : Clos Γ A B}
    {a : Wh Γ A}
    {b : Wh Γ B}
    → f ∙ᴷ a ⇓ b
    → `λ f ∙ a ⇓ b

  `app-neut :
    {f : Nu Γ (A `→ B)}
    {a : Wh Γ A}
    → `neut f ∙ a ⇓ `neut (f `∙ a)

data rec_of_else_⇓_ {Γ C} : Wh Γ `ℕ → Wh Γ C → Clos Γ C C → Wh Γ C → Set where
  `rec-zero :
    {cz : Wh Γ C}
    {cs : Clos Γ C C}
    → rec `zero of cz else cs ⇓ cz

  `rec-suc :
    {n : Wh Γ `ℕ}
    {cz : Wh Γ C}
    {cs : Clos Γ C C}
    {c c' : Wh Γ C}
    → rec n of cz else cs ⇓ c
    → cs ∙ᴷ c ⇓ c'
    → rec `suc n of cz else cs ⇓ c'

  `rec-neut :
    {n : Nu Γ `ℕ}
    {cz : Wh Γ C}
    {cs : Clos Γ C C}
    → rec `neut n of cz else cs ⇓ `neut (`rec n `of cz `else cs)

data _/ᴷ_⇓_ {Φ Γ} (σ : Env Φ Γ) : ∀{A B} → Clos Γ A B → Clos Φ A B → Set where
  `sub-clos : ∀{A B Δ}
    {f : Wh (Δ , A) B}
    {ρ : Env Γ Δ}
    {ρ' : Env Φ Δ}
    → σ ∘ ρ ⇓ ρ'
    → σ /ᴷ (ρ `/ f) ⇓ (ρ' `/ f)

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

data _/_⇓_ {Φ Γ} σ where
  `sub-zero : σ / `zero ⇓ `zero
  `sub-suc :
    {n : Wh Γ `ℕ}
    {n' : Wh Φ `ℕ}
    → σ / n ⇓ n'
    → σ / `suc n ⇓ `suc n'

  `sub-lam : ∀{A B}
    {f : Clos Γ A B}
    {f' : Clos Φ A B}
    → σ /ᴷ f ⇓ f'
    → σ / `λ f ⇓ `λ f'

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

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

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

  `sub-rec : ∀{C}
    {n : Nu Γ `ℕ}
    {cz : Wh Γ C}
    {cs : Clos Γ C C}
    {n' : Wh Φ `ℕ}
    {cz' : Wh Φ C}
    {cs' : Clos Φ C C}
    {c : Wh Φ C}
    → σ /ᴺ n ⇓ n'
    → σ / cz ⇓ cz'
    → σ /ᴷ cs ⇓ cs'
    → rec n' of cz' else cs'  ⇓ c
    → σ /ᴺ `rec n `of cz `else cs ⇓ c

  `sub-app : ∀{A B}
    {f : Nu Γ (A `→ B)}
    {a : Wh Γ A}
    {f' : Wh Φ (A `→ B)}
    {a' : Wh Φ A}
    {b' : Wh Φ B}
    → σ /ᴺ f ⇓ f'
    → σ / a ⇓ a'
    → f' ∙ a' ⇓ b'
    → σ /ᴺ f `∙ a ⇓ b'

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

data _!_ {Φ A B} : Clos Φ A B → Wh (Φ , A) B → Set where
  `force : ∀{Γ} {σ : Env Φ Γ} {b : Wh (Γ , A) B} {b' : Wh (Φ , A) B}
    → ↑₁ σ / b ⇓ b'
    → (σ `/ b) ! b'

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

hsub-det : ∀{Φ Γ A}
  {σ : Env Φ Γ}
  {x : Wh Γ A}
  {y z : Wh Φ A}
  → σ / x ⇓ y
  → σ / x ⇓ z
  → y ≡ z

hsub-detᴺ : ∀{Φ Γ A}
  {σ : Env Φ Γ}
  {x : Nu Γ A}
  {y z : Wh Φ A}
  → σ /ᴺ x ⇓ y
  → σ /ᴺ x ⇓ z
  → y ≡ z

comp-det : ∀{Φ Δ Γ}
  {σ : Env Φ Δ}
  {ρ : Env Δ Γ}
  {ρ₁ ρ₂ : Env Φ Γ}
  → σ ∘ ρ ⇓ ρ₁
  → σ ∘ ρ ⇓ ρ₂
  → ρ₁ ≡ ρ₂
comp-det `comp-emp `comp-emp = refl
comp-det (`comp-ext ρ⇓ρ₁ a⇓a₁) (`comp-ext ρ⇓ρ₂ a⇓a₂)
  rewrite comp-det ρ⇓ρ₁ ρ⇓ρ₂ | hsub-det a⇓a₁ a⇓a₂
  = refl

hsub-detᴷ : ∀{Φ Γ A B}
  {σ : Env Φ Γ}
  {x : Clos Γ A B}
  {y z : Clos Φ A B}
  → σ /ᴷ x ⇓ y
  → σ /ᴷ x ⇓ z
  → y ≡ z
hsub-detᴷ (`sub-clos ρ⇓ρ₁) (`sub-clos ρ⇓ρ₂)
  rewrite comp-det ρ⇓ρ₁ ρ⇓ρ₂ = refl

app-detᴷ : ∀{Γ A B}
  {f : Clos Γ A B}
  {a : Wh Γ A}
  {b₁ b₂ : Wh Γ B}
  → f ∙ᴷ a ⇓ b₁
  → f ∙ᴷ a ⇓ b₂
  → b₁ ≡ b₂
app-detᴷ (`app-clos b⇓b₁) (`app-clos b⇓b₂)
  rewrite hsub-det b⇓b₁ b⇓b₂ = refl

app-det : ∀{Γ A B}
  {f : Wh Γ (A `→ B)}
  {a : Wh Γ A}
  {b₁ b₂ : Wh Γ B}
  → f ∙ a ⇓ b₁
  → f ∙ a ⇓ b₂
  → b₁ ≡ b₂
app-det (`app-lam b⇓b₁) (`app-lam b⇓b₂)
  rewrite app-detᴷ b⇓b₁ b⇓b₂ = refl
app-det `app-neut `app-neut = refl

rec-det : ∀{Γ C}
  {n : Wh Γ `ℕ}
  {cz : Wh Γ C}
  {cs : Clos Γ C C}
  {c₁ c₂ : Wh Γ C}
  → rec n of cz else cs ⇓ c₁
  → rec n of cz else cs ⇓ c₂
  → c₁ ≡ c₂
rec-det `rec-zero `rec-zero = refl
rec-det (`rec-suc c⇓c₁ cs⇓cs₁) (`rec-suc c⇓c₂ cs⇓cs₂)
  rewrite rec-det c⇓c₁ c⇓c₂ | app-detᴷ cs⇓cs₁ cs⇓cs₂
  = refl
rec-det `rec-neut `rec-neut = refl


hsub-det `sub-zero `sub-zero = refl
hsub-det (`sub-suc n⇓n₁) (`sub-suc n⇓n₂)
  rewrite hsub-det n⇓n₁ n⇓n₂ = refl
hsub-det (`sub-lam b⇓b₁) (`sub-lam b⇓b₂)
  rewrite hsub-detᴷ b⇓b₁ b⇓b₂ = refl
hsub-det (`sub-neut x⇓y) (`sub-neut x⇓z) = hsub-detᴺ x⇓y x⇓z

hsub-detᴺ (`sub-var i) (`sub-var .i) = refl
hsub-detᴺ (`sub-app f⇓f₁ a⇓a₁ b⇓b₁) (`sub-app f⇓f₂ a⇓a₂ b⇓b₂)
  rewrite hsub-detᴺ f⇓f₁ f⇓f₂ | hsub-det a⇓a₁ a⇓a₂ | app-det b⇓b₁ b⇓b₂
  = refl
hsub-detᴺ (`sub-rec n⇓n₁ cz⇓cz₁ cs⇓cs₁ c⇓c₁) (`sub-rec n⇓n₂ cz⇓cz₂ cs⇓cs₂ c⇓c₂)
  rewrite hsub-detᴺ n⇓n₁ n⇓n₂ | hsub-det cz⇓cz₁ cz⇓cz₂ | hsub-detᴷ cs⇓cs₁ cs⇓cs₂ | rec-det c⇓c₁ c⇓c₂
  = refl

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

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 : ∀{m Γ A} (a : Val m Γ A) → ren idRen a ≡ a
id-renᴺ : ∀{m Γ A} (a : Neut m Γ A) → renᴺ idRen a ≡ a

id-renˢ : ∀{Φ Γ} (σ : Env Φ Γ) → renˢ idRen σ ≡ σ
id-renˢ ∅ = refl
id-renˢ (σ , a) rewrite id-renˢ σ | id-ren a = refl

id-renᴮ : ∀{m Γ A B} (a : Bind m Γ A B) → renᴮ idRen a ≡ a
id-renᴮ (`val b) rewrite id-ren b = refl
id-renᴮ (σ `/ b) rewrite id-renˢ σ = refl

id-ren `zero = refl
id-ren (`suc n) rewrite id-ren n = refl
id-ren (`λ b) rewrite id-renᴮ b = 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ᴺ (`rec n `of cz `else cs)
  rewrite id-renᴺ n | id-ren cz | id-renᴮ cs = refl

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

infix 1 _≈_
infix 1 _≈ᴺ_

data _≈_ {Γ} : ∀{A} (a a' : Wh Γ A) → Set
data _≈ᴺ_ {Γ} : ∀{A} (a a' : Nu Γ A) → Set

data _≈ᴷ_ {Γ} : ∀{A B} (f f' : Clos Γ A B) → Set where
  `conv-clos-eq : ∀{A B}
    {f g : Clos Γ A B}
    → f ≡ g
    → f ≈ᴷ g

  `conv-clos-kappa : ∀{A B}
    {f g : Clos Γ A B}
    {f' g' : Wh (Γ , A) B}
    → f ≢ g
    → f ! f'
    → g ! g'
    → f' ≈ g'
    → f ≈ᴷ g

data _≈_ {Γ} where
  `conv-zero : `zero ≈ `zero
  `conv-suc :
    {n n' : Wh Γ `ℕ}
    → n ≈ n'
    → `suc n ≈ `suc n'

  `conv-lam : ∀{A B}
    {f g : Clos Γ A B}
    → f ≈ᴷ g
    → `λ f ≈ `λ g

  `conv-neut : ∀{A} {a : Nu Γ A} {a' : Nu Γ A}
    → a ≈ᴺ a'
    → `neut a ≈ `neut a'

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

  `conv-rec : ∀{C}
    {n : Nu Γ `ℕ}
    {cz : Wh Γ C}
    {cs : Clos Γ C C}
    {n' : Nu Γ `ℕ}
    {cz' : Wh Γ C}
    {cs' : Clos Γ C C}
    → n ≈ᴺ n'
    → cz ≈ cz'
    → cs ≈ᴷ cs'
    → `rec n `of cz `else cs ≈ᴺ `rec n' `of cz' `else cs'

  `conv-app : ∀{A B}
    {f : Nu Γ (A `→ B)}
    {a : Wh Γ A}
    {f' : Nu Γ (A `→ B)}
    {a' : Wh Γ A}
    → f ≈ᴺ f'
    → a ≈ a'
    → f `∙ a ≈ᴺ f' `∙ a'

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

`refl : ∀{Γ A} (x : Wh Γ A) → x ≈ x
`reflᴺ : ∀{Γ A} (x : Nu Γ A) → x ≈ᴺ x

`reflᴷ : ∀{Γ A B} (k : Clos Γ A B) → k ≈ᴷ k
`reflᴷ (σ `/ b) = `conv-clos-eq refl

`refl `zero = `conv-zero
`refl (`suc n) = `conv-suc (`refl n)
`refl (`λ b) = `conv-lam (`reflᴷ b)
`refl (`neut a) = `conv-neut (`reflᴺ a)

`reflᴺ (`var i) = `conv-var i
`reflᴺ (f `∙ a) = `conv-app (`reflᴺ f) (`refl a)
`reflᴺ (`rec n `of cz `else cs) = `conv-rec (`reflᴺ n) (`refl cz) (`reflᴷ cs)

`refl-eq : ∀{Γ A} (x y : Wh Γ A) → x ≡ y → x ≈ y
`refl-eq x .x refl = `refl x

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

`sym : ∀{Γ A} {x y : Wh Γ A} → x ≈ y → y ≈ x
`symᴺ : ∀{Γ A} {x y : Nu Γ A} → x ≈ᴺ y → y ≈ᴺ x

`symᴷ : ∀{Γ A B} {j k : Clos Γ A B} → j ≈ᴷ k → k ≈ᴷ j
`symᴷ (`conv-clos-eq refl) = `conv-clos-eq refl
`symᴷ (`conv-clos-kappa f≢g f⇓f' g⇓g' f'≈g') = `conv-clos-kappa (nsym f≢g) g⇓g' f⇓f' (`sym f'≈g')

`sym `conv-zero = `conv-zero
`sym (`conv-suc n) = `conv-suc (`sym n)
`sym (`conv-lam b≈b') = `conv-lam (`symᴷ b≈b')
`sym (`conv-neut x≈y) = `conv-neut (`symᴺ x≈y)

`symᴺ (`conv-var i) = `conv-var i
`symᴺ (`conv-app f≈f' a≈a') = `conv-app (`symᴺ f≈f') (`sym a≈a')
`symᴺ (`conv-rec n≈n' cz≈cz' cs≈cs') = `conv-rec (`symᴺ n≈n') (`sym cz≈cz') (`symᴷ cs≈cs')

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

`trans : ∀{Γ A} {x y z : Wh Γ A}
  → x ≈ z
  → z ≈ y
  → x ≈ y
`transᴺ : ∀{Γ A} {x y z : Nu Γ A}
  → x ≈ᴺ z
  → z ≈ᴺ y
  → x ≈ᴺ y

`transᴷ : ∀{Γ A B} {x y z : Clos Γ A B}
  → x ≈ᴷ z
  → z ≈ᴷ y
  → x ≈ᴷ y
`transᴷ (`conv-clos-eq refl) (`conv-clos-eq refl) = `conv-clos-eq refl
`transᴷ (`conv-clos-eq refl) (`conv-clos-kappa h≢g h⇓h g⇓g' h'≈g') = `conv-clos-kappa h≢g h⇓h g⇓g' h'≈g'
`transᴷ (`conv-clos-kappa f≢g f⇓f' h⇓h f'≈h') (`conv-clos-eq refl) = `conv-clos-kappa f≢g f⇓f' h⇓h f'≈h'
`transᴷ (`conv-clos-kappa {f = f} _ f⇓f' (`force h⇓h₁) f'≈h') (`conv-clos-kappa {g = g} _ (`force h⇓h₂) g⇓g' h'≈g')
  with eq-decᴷ f g
... | yes f≡g
  = `conv-clos-eq f≡g
... | no f≢g
  rewrite hsub-det h⇓h₁ h⇓h₂
  = `conv-clos-kappa f≢g f⇓f' g⇓g' (`trans f'≈h' h'≈g')

`trans `conv-zero `conv-zero = `conv-zero
`trans (`conv-suc x≈z) (`conv-suc z≈y) = `conv-suc (`trans x≈z z≈y)
`trans (`conv-lam x≈z) (`conv-lam z≈y) = `conv-lam (`transᴷ x≈z z≈y)
`trans (`conv-neut x≈z) (`conv-neut z≈y) = `conv-neut (`transᴺ x≈z z≈y)

`transᴺ (`conv-var i) y₁ = y₁
`transᴺ (`conv-app x x₁) (`conv-app x₂ x₃) = `conv-app (`transᴺ x x₂) (`trans x₁ x₃)
`transᴺ (`conv-rec x x₁ x₂) (`conv-rec x₃ x₄ x₅) = `conv-rec (`transᴺ x x₃) (`trans x₁ x₄) (`transᴷ x₂ x₅)

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

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

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

⟦ Γ ⊢ `ℕ ∶ʳ `zero ⟧ = ⊤
⟦ Γ ⊢ `ℕ ∶ʳ `suc n ⟧ = ⟦ Γ ⊢ `ℕ ∶ʳ n ⟧
⟦ Γ ⊢ (A `→ B) ∶ʳ `λ f ⟧ = ⟦ Γ ⊩ A ⇒ B ∶ʳ f ⟧
⟦ Γ ⊢ A ∶ʳ `neut a ⟧ = ∃ λ a' → a ≈ᴺ embᴺ a'

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 : Wh Γ A) → Set
⟦ Φ ⊢ Γ ∶ʳ σ / A ∶ʳ a ⟧ = ∃ λ a' → σ / a ⇓ a' ∧ ⟦ Φ ⊢ a' ∶ A ⟧

Sub-Model = ⟦_⊢_∶ʳ_/_∶ʳ_⟧
syntax Sub-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 : 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

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

⟦var⟧ : ∀{Φ Γ A} {σ : Env Φ Γ}
  (⟦σ⟧ : ⟦ Φ ⊨ σ ∶ Γ ⟧) (i : Var Γ A)
  → ⟦ Φ ⊢ σ ∶ Γ / `neut (`var i) ∶ A ⟧
⟦var⟧ {σ = σ} ⟦σ⟧ i = lookup σ i , `sub-neut (`sub-var 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 : Wh Γ A)
  → ren Δ≥Φ (ren Φ≥Γ a) ≡ ren (comp Δ≥Φ Φ≥Γ) a

comp-renᴺ : ∀{Γ Φ Δ A}
  (Δ≥Φ : Ren Δ Φ)
  (Φ≥Γ : Ren Φ Γ)
  (a : Nu Γ 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 Φ Γ)
  (k : Clos Γ A B)
  → renᴮ Δ≥Φ (renᴮ Φ≥Γ k) ≡ renᴮ (comp Δ≥Φ Φ≥Γ) k
comp-renᴷ Δ≥Φ Φ≥Γ (σ `/ b) rewrite comp-renˢ Δ≥Φ Φ≥Γ σ = refl

comp-ren Δ≥Φ Φ≥Γ `zero = refl
comp-ren Δ≥Φ Φ≥Γ (`suc n) rewrite comp-ren Δ≥Φ Φ≥Γ n = refl
comp-ren Δ≥Φ Φ≥Γ (`λ b) rewrite comp-renᴷ Δ≥Φ Φ≥Γ b = 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ᴺ Δ≥Φ Φ≥Γ (`rec n `of cz `else 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 : 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 : Wh Γ A} {a' : Wh Φ A} {σ : Env Φ Γ}
  (Δ≥Φ : Ren Δ Φ) → σ / a ⇓ a' → renˢ Δ≥Φ σ / a ⇓ ren Δ≥Φ a'
renᴺ-hsub : ∀{Φ Δ Γ A} {a : Nu Γ A} {a' : 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} {k : Clos Γ A B} {k' : Clos Φ A B} {σ : Env Φ Γ}
  (Δ≥Φ : Ren Δ Φ) → σ /ᴷ k ⇓ k' → renˢ Δ≥Φ σ /ᴷ k ⇓ renᴮ Δ≥Φ k'
renᴷ-hsub Δ≥Φ (`sub-clos ρ⇓ρ') = `sub-clos (renˢ-hsub Δ≥Φ ρ⇓ρ')

ren-appᴷ : ∀{Δ Γ A B} {f : Clos Γ A B} {a : Wh Γ A} {b : Wh Γ B}
  (Δ≥Γ : Ren Δ Γ) → f ∙ᴷ a ⇓ b → renᴮ Δ≥Γ f ∙ᴷ ren Δ≥Γ a ⇓ ren Δ≥Γ b
ren-appᴷ Δ≥Γ (`app-clos b⇓b') = `app-clos (ren-hsub Δ≥Γ b⇓b')

ren-app : ∀{Δ Γ A B} {f : Wh Γ (A `→ B)} {a : Wh Γ A} {b : Wh Γ B}
  (Δ≥Γ : Ren Δ Γ) → f ∙ a ⇓ b → ren Δ≥Γ f ∙ ren Δ≥Γ a ⇓ ren Δ≥Γ b
ren-app Δ≥Γ (`app-lam k⇓k') = `app-lam (ren-appᴷ Δ≥Γ k⇓k')
ren-app Δ≥Γ `app-neut = `app-neut

ren-rec : ∀{Δ Γ C} {n : Wh Γ `ℕ} {cz : Wh Γ C} {cs : Clos Γ C C} {c : Wh Γ C}
  (Δ≥Γ : Ren Δ Γ) → rec n of cz else cs ⇓ c → rec (ren Δ≥Γ n) of (ren Δ≥Γ cz) else (renᴮ Δ≥Γ cs) ⇓ ren Δ≥Γ c
ren-rec Δ≥Γ `rec-zero = `rec-zero
ren-rec Δ≥Γ (`rec-suc c⇓c' cs⇓cs') = `rec-suc (ren-rec Δ≥Γ c⇓c') (ren-appᴷ Δ≥Γ cs⇓cs')
ren-rec Δ≥Γ `rec-neut = `rec-neut

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

ren-hsub Δ≥Φ `sub-zero = `sub-zero
ren-hsub Δ≥Φ (`sub-suc n⇓n') = `sub-suc (ren-hsub Δ≥Φ n⇓n')
ren-hsub Δ≥Φ (`sub-lam k⇓k') = `sub-lam (renᴷ-hsub Δ≥Φ k⇓k')
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-app f⇓f' a⇓a' b⇓b' )
  = `sub-app (renᴺ-hsub Δ≥Φ f⇓f') (ren-hsub Δ≥Φ a⇓a') (ren-app Δ≥Φ b⇓b')
renᴺ-hsub Δ≥Φ (`sub-rec n⇓n' cz⇓cz' cs⇓cs' c⇓c')
  = `sub-rec (renᴺ-hsub Δ≥Φ n⇓n') (ren-hsub Δ≥Φ cz⇓cz') (renᴷ-hsub Δ≥Φ cs⇓cs') (ren-rec Δ≥Φ  c⇓c')

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

ren-conv : ∀{Δ Γ A} {a a' : Wh Γ A} (Δ≥Γ : Ren Δ Γ) → a ≈ a' → ren Δ≥Γ a ≈ ren Δ≥Γ a'
ren-convᴺ : ∀{Δ Γ A} {a a' : Nu Γ A} (Δ≥Γ : Ren Δ Γ) → a ≈ᴺ a' → renᴺ Δ≥Γ a ≈ᴺ renᴺ Δ≥Γ a'

ren-convᴷ : ∀{Δ Γ A B} {k k' : Clos Γ A B} (Δ≥Γ : Ren Δ Γ) → k ≈ᴷ k' → renᴮ Δ≥Γ k ≈ᴷ renᴮ Δ≥Γ k'
ren-convᴷ Δ≥Γ (`conv-clos-eq {f = σ `/ b} refl) = `conv-clos-eq refl
ren-convᴷ Δ≥Γ (`conv-clos-kappa {A = A} _ (`force {σ = σ} {b = f} f⇓f') (`force {σ = ρ} {b = g} g⇓g') f'≈g')
  with eq-decᴷ (renˢ Δ≥Γ σ `/ f) (renˢ Δ≥Γ ρ `/ g)
... | yes f≡g rewrite f≡g
  = `conv-clos-eq refl
... | no f≢g
  with ren-hsub (keep Δ≥Γ) f⇓f'
... | qf
  with ren-hsub (keep Δ≥Γ) g⇓g'
... | qg
  with ren-conv (keep Δ≥Γ) f'≈g'
... | ih
  rewrite sym (renˢ-comp A σ Δ≥Γ) | sym (renˢ-comp A ρ Δ≥Γ)
  = `conv-clos-kappa f≢g (`force qf) (`force qg) ih

ren-conv Δ≥Γ `conv-zero = `conv-zero
ren-conv Δ≥Γ (`conv-suc n≈n') = `conv-suc (ren-conv Δ≥Γ n≈n')
ren-conv Δ≥Γ (`conv-lam k≈k') = `conv-lam (ren-convᴷ Δ≥Γ k≈k')
ren-conv Δ≥Γ (`conv-neut a≈a') = `conv-neut (ren-convᴺ Δ≥Γ a≈a')

ren-convᴺ Δ≥Γ (`conv-var i) = `conv-var (renᴿ Δ≥Γ i)
ren-convᴺ Δ≥Γ (`conv-rec n≈n' cz≈cz' cs≈cs')
  = `conv-rec (ren-convᴺ Δ≥Γ n≈n') (ren-conv Δ≥Γ cz≈cz') (ren-convᴷ Δ≥Γ cs≈cs')
ren-convᴺ Δ≥Γ (`conv-app f≈f' a≈a')
  = `conv-app (ren-convᴺ Δ≥Γ f≈f') (ren-conv Δ≥Γ a≈a')

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

reflect : ∀{Γ} A
  {a : Nu Γ A}
  (a' : Ne Γ A)
  (a≈a' : a ≈ᴺ embᴺ a')
  → ⟦ Γ ⊢ `neut a ∶ A ⟧
reflect `ℕ n' n≈n' = n' , n≈n'
reflect (A `→ B) f' f≈f' = f' , f≈f'

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

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

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

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

hsub-id : ∀{Γ A} (a : Wh Γ A) → idEnv / a ⇓ a
hsub-idᴺ : ∀{Γ A} (a : Nu Γ A) → idEnv /ᴺ a ⇓ `neut a

hsub-comp : ∀{Φ Γ} (σ : Env Φ Γ) → idEnv ∘ σ ⇓ σ
hsub-comp ∅ = `comp-emp
hsub-comp (σ , a) = `comp-ext (hsub-comp σ) (hsub-id a)

hsub-idᴷ : ∀{Γ A B} (k : Clos Γ A B) → idEnv /ᴷ k ⇓ k
hsub-idᴷ (σ `/ b) = `sub-clos (hsub-comp σ)

hsub-id `zero = `sub-zero
hsub-id (`suc n) = `sub-suc (hsub-id n)
hsub-id (`λ k) = `sub-lam (hsub-idᴷ k)
hsub-id (`neut a) = `sub-neut (hsub-idᴺ a)

hsub-idᴺ (`var i) rewrite id-lookup i = `sub-var i
hsub-idᴺ (f `∙ a) = `sub-app (hsub-idᴺ f) (hsub-id a) `app-neut
hsub-idᴺ (`rec b `of cz `else cs) = `sub-rec (hsub-idᴺ b) (hsub-id cz) (hsub-idᴷ cs) `rec-neut

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

-- commutativity of emb and ren wrt conv
emb-ren-sym : ∀{Γ Δ A} (Δ≥Γ : Ren Δ Γ) (a : Nf Γ A) → emb (ren Δ≥Γ a) ≈ ren Δ≥Γ (emb a)
emb-ren-symᴺ : ∀{Γ Δ A} (Δ≥Γ : Ren Δ Γ) (a : Ne Γ A) → embᴺ (renᴺ Δ≥Γ a) ≈ᴺ renᴺ Δ≥Γ (embᴺ a)

emb-ren-symᴮ : ∀{Γ Δ A B} (Δ≥Γ : Ren Δ Γ) (b : Bind nf Γ A B) → embᴮ (renᴮ Δ≥Γ b) ≈ᴷ renᴮ Δ≥Γ (embᴮ b)
emb-ren-symᴮ {A = A} Δ≥Γ (`val b)
  with eq-decᴷ (idEnv `/ emb (ren (keep Δ≥Γ) b)) (renˢ Δ≥Γ idEnv `/ emb b)
... | yes k≡k'
  = `conv-clos-eq k≡k'
... | no k≢k'
  with ren-hsub (keep Δ≥Γ) (hsub-id (emb b))
... | q
  rewrite sym (renˢ-comp A idEnv Δ≥Γ)
  = `conv-clos-kappa
  k≢k'
  (`force (hsub-id (emb (ren (keep Δ≥Γ) b))))
  (`force q)
  (emb-ren-sym (keep Δ≥Γ) b)

emb-ren-sym Δ≥Γ `zero = `conv-zero
emb-ren-sym Δ≥Γ (`suc n) = `conv-suc (emb-ren-sym Δ≥Γ n)
emb-ren-sym Δ≥Γ (`λ b) = `conv-lam (emb-ren-symᴮ Δ≥Γ b)

emb-ren-sym Δ≥Γ (`neut a) = `conv-neut (emb-ren-symᴺ Δ≥Γ a)

emb-ren-symᴺ Δ≥Γ (`var i) = `conv-var (renᴿ Δ≥Γ i)
emb-ren-symᴺ Δ≥Γ (f `∙ a) = `conv-app (emb-ren-symᴺ Δ≥Γ f) (emb-ren-sym Δ≥Γ a)
emb-ren-symᴺ Δ≥Γ (`rec n `of cz `else cs) = `conv-rec (emb-ren-symᴺ Δ≥Γ n) (emb-ren-sym Δ≥Γ cz) (emb-ren-symᴮ Δ≥Γ cs)

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

reify : ∀{Γ} A
  (a : Wh Γ A)
  (⟦a⟧ : ⟦ Γ ⊢ a ∶ A ⟧)
  → ∃ λ a'
  → a ≈ emb a'

reify `ℕ `zero tt = `zero , `conv-zero
reify `ℕ (`suc n) ⟦n⟧
  with reify `ℕ n ⟦n⟧
... | n' , n≈n'
  = `suc n' , `conv-suc n≈n'
reify `ℕ (`neut n) (n' , n≈n') = `neut n' , `conv-neut n≈n'
reify (A `→ B) (`neut f) (f' , f≈f') = `neut f' , `conv-neut f≈f'

reify (A `→ B) (`λ (σ `/ b)) ⟦f⟧
  with ⟦f⟧ (skip idRen) `x (reflect A `xᴺ (`conv-var here))
... | b' , b⇓b' , ⟦b⟧
  with reify B _ ⟦b⟧
... | b'' , b'≈b''
  with eq-decᴷ (σ `/ b) (idEnv `/ emb b'')
... | yes b≡b''
  = `λ (`val b'') , `conv-lam (`conv-clos-eq b≡b'')
... | no b≢b''
  = `λ (`val b'') , `conv-lam (`conv-clos-kappa b≢b'' (`force b⇓b') (`force (hsub-id (emb b''))) b'≈b'')

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

⟦zero⟧ : ∀{Φ Γ σ} → ⟦ Φ ⊢ σ ∶ Γ / `zero ∶ `ℕ ⟧
⟦zero⟧ = `zero , `sub-zero , tt

⟦suc⟧ : ∀{Φ Γ σ n}
  → ⟦ Φ ⊢ σ ∶ Γ / n ∶ `ℕ ⟧
  → ⟦ Φ ⊢ σ ∶ Γ / `suc n ∶ `ℕ ⟧
⟦suc⟧ (n' , n⇓n' , ⟦n⟧) = `suc n' , `sub-suc n⇓n' , ⟦n⟧

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

⟦λ⟧ : ∀{Φ Γ σ A B k}
  → ⟦ Φ ⊩ σ ∶ Γ / k ∶ A ⇒ B ⟧
  → ⟦ Φ ⊢ σ ∶ Γ / `λ k ∶ A `→ B ⟧
⟦λ⟧ (k' , k⇓k' , ⟦k⟧) = `λ k' , `sub-lam k⇓k' , ⟦k⟧

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

⟦app⟧ : ∀{Γ A B} f a
  → ⟦ Γ ⊢ f ∶ A `→ B ⟧
  → ⟦ Γ ⊢ a ∶ A ⟧
  → ∃ λ b
  → f ∙ a ⇓ b
  ∧ ⟦ Γ ⊢ b ∶ B ⟧

⟦app⟧ (`neut f) a (f' , f≈f') ⟦a⟧
  with reify _ a ⟦a⟧
... | a' , a≈a'
  = `neut (f `∙ a)
  , `app-neut
  , reflect _ (f' `∙ a') (`conv-app f≈f' a≈a')

⟦app⟧ (`λ (σ `/ b)) a ⟦f⟧ ⟦a⟧
  with ⟦f⟧ idRen a ⟦a⟧
... | b' , b⇓b' , ⟦b⟧
  rewrite id-renˢ σ
  = b'
  , `app-lam (`app-clos b⇓b')
  , ⟦b⟧

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

_⟦∙⟧_ : ∀{Φ Γ A B σ f a}
  → ⟦ Φ ⊢ σ ∶ Γ / `neut f ∶ A `→ B ⟧
  → ⟦ Φ ⊢ σ ∶ Γ / a ∶ A ⟧
  → ⟦ Φ ⊢ σ ∶ Γ / `neut (f `∙ a) ∶ B ⟧
(f' , `sub-neut f⇓f' , ⟦f⟧) ⟦∙⟧ (a' , a⇓a' , ⟦a⟧)
  with ⟦app⟧ f' a' ⟦f⟧ ⟦a⟧
... | b , b⇓b' , ⟦b⟧
  = b
  , `sub-neut (`sub-app f⇓f' a⇓a' b⇓b')
  , ⟦b⟧

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

⟦rec⟧ : ∀{Γ C} n cz cs
  → ⟦ Γ ⊢ n ∶ `ℕ ⟧
  → ⟦ Γ ⊢ cz ∶ C ⟧
  → ⟦ Γ ⊩ cs ∶ C ⇒ C ⟧
  → ∃ λ c
  → rec n of cz else 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-clos 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ᴺ (`conv-var here))
... | c , cs⇓c , ⟦c⟧
  with reify C c ⟦c⟧
... | c' , c≈c'
  with eq-decᴷ (σ `/ cs) (idEnv `/ emb c')
... | yes cs≡c'
  = `neut (`rec n `of cz `else (σ `/ cs))
  , `rec-neut
  , reflect C (`rec n' `of cz' `else (`val c'))
    (`conv-rec n≈n' cz≈cz' (`conv-clos-eq cs≡c'))
... | no cs≢c'
  = `neut (`rec n `of cz `else (σ `/ cs))
  , `rec-neut
  , reflect C (`rec n' `of cz' `else (`val c'))
    (`conv-rec n≈n' cz≈cz' (`conv-clos-kappa cs≢c' (`force cs⇓c) (`force (hsub-id (emb c'))) c≈c'))

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

⟦rec⟧_⟦of⟧_⟦else⟧ : ∀{Φ Γ C σ n cz cs}
  → ⟦ Φ ⊢ σ ∶ Γ / `neut n ∶ `ℕ ⟧
  → ⟦ Φ ⊢ σ ∶ Γ / cz ∶ C ⟧
  → ⟦ Φ ⊩ σ ∶ Γ / cs ∶ C ⇒ C ⟧
  → ⟦ Φ ⊢ σ ∶ Γ / `neut (`rec n `of cz `else cs) ∶ C ⟧

⟦rec⟧ (n' , `sub-neut n⇓n' , ⟦n⟧) ⟦of⟧ (cz' , cz⇓cz' , ⟦cz⟧) ⟦else⟧ (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 : Wh Γ A)
  (⟦a⟧ : ⟦ Γ ⊢ a ∶ A ⟧)
  → ⟦ Δ ⊢ ren Δ≥Γ a ∶ A ⟧

mono Δ≥Γ `ℕ `zero tt = tt
mono Δ≥Γ `ℕ (`suc n) ⟦n⟧ = mono Δ≥Γ `ℕ n ⟦n⟧
mono Δ≥Γ `ℕ (`neut b) (b' , b≈b')
  = renᴺ Δ≥Γ b' , `transᴺ (ren-convᴺ Δ≥Γ b≈b') (`symᴺ (emb-ren-symᴺ Δ≥Γ b'))
mono Δ≥Γ (A `→ B) (`neut f) (f' , f≈f')
  = renᴺ Δ≥Γ f' , `transᴺ (ren-convᴺ Δ≥Γ f≈f') (`symᴺ (emb-ren-symᴺ Δ≥Γ 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 : Wh Γ A)
  → ⟦ Φ ⊢ σ ∶ Γ / a ∶ A ⟧

⟦hsubᴺ⟧ : ∀{Φ Γ A}
  {σ : Env Φ Γ}
  (⟦σ⟧ : ⟦ Φ ⊨ σ ∶ Γ ⟧)
  (a : Nu Γ 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 Φ Γ}
  (⟦σ⟧ : ⟦ Φ ⊨ σ ∶ Γ ⟧)
  (k : Clos Γ A B)
  → ⟦ Φ ⊩ σ ∶ Γ / k ∶ A ⇒ B ⟧
⟦hsubᴷ⟧ ⟦σ⟧ (ρ `/ b)
  with ⟦comp⟧ ⟦σ⟧ ρ
... | ρ' , ρ⇓ρ' , ⟦ρ⟧
  = ρ' `/ b , `sub-clos ρ⇓ρ' , λ Δ≥Φ a ⟦a⟧ → ⟦hsub⟧ (monos Δ≥Φ ⟦ρ⟧ , ⟦a⟧) b

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

⟦hsub⟧ ⟦σ⟧ `zero = ⟦zero⟧
⟦hsub⟧ ⟦σ⟧ (`suc n) = ⟦suc⟧ (⟦hsub⟧ ⟦σ⟧ n)
⟦hsub⟧ ⟦σ⟧ (`λ k) = ⟦λ⟧ (⟦hsubᴷ⟧ ⟦σ⟧ k)
⟦hsub⟧ ⟦σ⟧ (`neut a) = ⟦hsubᴺ⟧ ⟦σ⟧ a
⟦hsubᴺ⟧ {σ = σ} ⟦σ⟧ (`var i) = ⟦var⟧ ⟦σ⟧ i
⟦hsubᴺ⟧ ⟦σ⟧ (f `∙ a) = ⟦hsubᴺ⟧ ⟦σ⟧ f ⟦∙⟧ ⟦hsub⟧ ⟦σ⟧ a
⟦hsubᴺ⟧ ⟦σ⟧ (`rec n `of cz `else cs) = ⟦rec⟧ ⟦hsubᴺ⟧ ⟦σ⟧ n ⟦of⟧ ⟦hsub⟧ ⟦σ⟧ cz ⟦else⟧ (⟦hsubᴷ⟧ ⟦σ⟧ cs)

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

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

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

hsub-id-det : ∀{Γ A} {a a' : Wh Γ A} → idEnv / a ⇓ a' → a ≡ a'
hsub-id-det {a = a} = hsub-det (hsub-id a)

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

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

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

norm : ∀{Γ A} (a : Wh Γ A) → ∃ λ a' → a ≈ emb a'
norm a with hsub idEnv a
... | a' , a⇓a' , a'' , a'≈a''
  rewrite hsub-id-det a⇓a'
  = a'' , a'≈a''

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

nf-conv-eq : ∀{Γ A} (x y : Nf Γ A) → emb x ≈ emb y → x ≡ y
nf-conv-eqᴺ : ∀{Γ A} (x y : Ne Γ A) → embᴺ x ≈ᴺ embᴺ y → x ≡ y

nf-conv-eqᴮ : ∀{Γ A B} (x y : Bind nf Γ A B) → embᴮ x ≈ᴷ embᴮ y → x ≡ y
nf-conv-eqᴮ (`val f) (`val g) (`conv-clos-eq f≡g)
  rewrite nf-conv-eq f g (`refl-eq (emb f) (emb g) (inj-clos₃ f≡g))
  = refl
nf-conv-eqᴮ (`val f) (`val g) (`conv-clos-kappa f≢g (`force f⇓f') (`force g⇓g') f'≈g')
  rewrite sym (hsub-id-det f⇓f') | sym (hsub-id-det g⇓g') | nf-conv-eq f g f'≈g'
  = refl

nf-conv-eq `zero `zero x≈y = refl
nf-conv-eq `zero (`suc n) ()
nf-conv-eq `zero (`neut y) ()
nf-conv-eq (`suc n) `zero ()
nf-conv-eq (`suc m) (`suc n) (`conv-suc m≈n)
  rewrite nf-conv-eq m n m≈n
  = refl
nf-conv-eq (`suc n) (`neut y) ()
nf-conv-eq (`λ j) (`λ k) (`conv-lam j≈k)
  rewrite nf-conv-eqᴮ j k j≈k
  = refl
nf-conv-eq (`λ (`val b)) (`neut y) ()
nf-conv-eq (`neut x) `zero ()
nf-conv-eq (`neut x) (`suc n) ()
nf-conv-eq (`neut x) (`λ (`val b)) ()
nf-conv-eq (`neut x) (`neut y) (`conv-neut x≈y)
  rewrite nf-conv-eqᴺ x y x≈y
  = refl
nf-conv-eqᴺ (`var i) (`var .i) (`conv-var .i) = refl
nf-conv-eqᴺ (f₁ `∙ a₁) (f₂ `∙ a₂) (`conv-app f₁≈f₂ a₁≈a₂)
  rewrite nf-conv-eqᴺ f₁ f₂ f₁≈f₂ | nf-conv-eq a₁ a₂ a₁≈a₂
  = refl
nf-conv-eqᴺ (`rec b₁ `of cz₁ `else cs₁) (`rec b₂ `of cz₂ `else cs₂) (`conv-rec b₁≈b₂ cz₁≈cz₂ cs₁≈cs₂)
  rewrite nf-conv-eqᴺ b₁ b₂ b₁≈b₂ | nf-conv-eq cz₁ cz₂ cz₁≈cz₂ | nf-conv-eqᴮ cs₁ cs₂ cs₁≈cs₂
  = refl
nf-conv-eqᴺ (`var i) (y `∙ a) ()
nf-conv-eqᴺ (`var i) (`rec y `of ct `else cf) ()
nf-conv-eqᴺ (x `∙ a) (`var i) ()
nf-conv-eqᴺ (x `∙ a) (`rec y `of ct `else cf) ()
nf-conv-eqᴺ (`rec x `of ct `else cf) (`var i) ()
nf-conv-eqᴺ (`rec x `of ct `else cf) (y `∙ a) ()

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

conv-dec : ∀{Γ A} (x y : Wh Γ A) → Dec (x ≈ y)
conv-dec x y
  with norm x | norm y
... | x' , x≈x' | y' , y≈y'
  with eq-dec x' y'
... | yes x'≡y' rewrite x'≡y'
  = yes (`trans x≈x' (`sym y≈y'))
... | no f
  = no (λ x≈y → f (nf-conv-eq x' y' (`trans (`sym x≈x') (`trans x≈y y≈y'))))

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

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 → 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 → Wh Φ A
eval σ a = proj₁ (⟦hsub⟧ (reflects σ) (wnorm a))

enorm : ∀{Γ A} → Exp Γ A → Nf Γ A
enorm a with hsub idEnv (wnorm a)
... | a' , a⇓a' , a'' , a'≈a'' = a''

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