RenSub.agda

-- Inspired by
-- https://github.com/andreasabel/strong-normalization/blob/master/agda/RenamingAndSubstitution.agda
-- and
-- https://github.com/mietek/coquand

{-# OPTIONS --no-positivity-check #-}

module RenSub where

open import Function public
  using (_∘_ ; case_of_)

open import Relation.Binary.PropositionalEquality public
  using (_≡_ ; refl ; cong ; subst ; sym ; trans ; module ≡-Reasoning)
  renaming (cong₂ to cong²)


-- Types
infixr 7 _⊃_
data 𝒯 : Set where
  •   : 𝒯
  _⊃_ : (A B : 𝒯) →
        𝒯

-- Contexts
data 𝒞 : Set where
  []    : 𝒞
  [_,_] : (Γ : 𝒞) (A : 𝒯) →
          𝒞

-- Variables
infix 4 _∋_
data _∋_ : 𝒞 → 𝒯 → Set where
  zero : ∀ {Γ A} →
           [ Γ , A ] ∋ A
  suc  : ∀ {Γ A B} →
           (x : Γ ∋ A) →
           [ Γ , B ] ∋ A

-- Terms
infix 3 _⊢_
data _⊢_ : 𝒞 → 𝒯 → Set where
  ν   : ∀ {Γ A} →
          (i : Γ ∋ A) →
          Γ ⊢ A
  ƛ   : ∀ {Γ A B} →
          (M : [ Γ , A ] ⊢ B) →
          Γ ⊢ A ⊃ B
  _∙_ : ∀ {Γ A B} →
          (M : Γ ⊢ A ⊃ B) (N : Γ ⊢ A) →
          Γ ⊢ B


--------------------------------------------------------------------------------
--
-- Renamings

infix 4 _∋⋆_
data _∋⋆_ : 𝒞 → 𝒞 → Set where
  []    : ∀ {Γ} →
            Γ ∋⋆ []
  [_,_] : ∀ {Γ Δ A} →
            (xs : Δ ∋⋆ Γ) (x : Δ ∋ A) →
            Δ ∋⋆ [ Γ , A ]

putᵣ : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → Δ ∋⋆ Γ
putᵣ {[]}        f = []
putᵣ {[ Γ , A ]} f = [ putᵣ (λ i → f (suc i)) , f zero ]

getᵣ : ∀ {Γ Δ A} → Δ ∋⋆ Γ → Γ ∋ A → Δ ∋ A
getᵣ [ xs , x ] zero    = x
getᵣ [ xs , x ] (suc i) = getᵣ xs i

unwkᵣ : ∀ {Γ Δ A} → Δ ∋⋆ [ Γ , A ] → Δ ∋⋆ Γ
unwkᵣ [ xs , x ] = xs

wkᵣ : ∀ {A Γ Δ} → Δ ∋⋆ Γ → [ Δ , A ] ∋⋆ Γ
wkᵣ []         = []
wkᵣ [ xs , x ] = [ wkᵣ xs , suc x ]

liftᵣ : ∀ {A Γ Δ} → Δ ∋⋆ Γ → [ Δ , A ] ∋⋆ [ Γ , A ]
liftᵣ xs = [ wkᵣ xs , zero ]

idᵣ : ∀ {Γ} → Γ ∋⋆ Γ
idᵣ {[]}        = []
idᵣ {[ Γ , A ]} = liftᵣ idᵣ

ren : ∀ {Γ Δ A} → Δ ∋⋆ Γ → Γ ⊢ A → Δ ⊢ A
ren xs (ν i)   = ν (getᵣ xs i)
ren xs (ƛ M)   = ƛ (ren (liftᵣ xs) M)
ren xs (M ∙ N) = ren xs M ∙ ren xs N

wk : ∀ {A Γ C} → Γ ⊢ C → [ Γ , A ] ⊢ C
wk M = ren (wkᵣ idᵣ) M

-- Composition of renamings
_○_ : ∀ {Γ Δ Φ} → Φ ∋⋆ Δ → Δ ∋⋆ Γ → Φ ∋⋆ Γ
xs ○ []         = []
xs ○ [ ys , y ] = [ xs ○ ys , getᵣ xs y ]

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

module _ where
  open ≡-Reasoning

  wkgetᵣ : ∀ {Γ Δ A C} →
             (xs : Δ ∋⋆ Γ) (i : Γ ∋ C) →
             getᵣ (wkᵣ {A} xs) i ≡ suc (getᵣ xs i)
  wkgetᵣ [ xs , x ] zero    = refl
  wkgetᵣ [ xs , x ] (suc i) = wkgetᵣ xs i

  idgetᵣ : ∀ {Γ A} →
             (i : Γ ∋ A) →
             getᵣ idᵣ i ≡ i
  idgetᵣ zero    = refl
  idgetᵣ (suc i) = begin
                     getᵣ (wkᵣ idᵣ) i
                   ≡⟨ wkgetᵣ idᵣ i ⟩
                     suc (getᵣ idᵣ i)
                   ≡⟨ cong suc (idgetᵣ i) ⟩
                     suc i
                   ∎

  idren : ∀ {Γ A} →
            (M : Γ ⊢ A) →
            ren idᵣ M ≡ M
  idren (ν i)   = cong ν (idgetᵣ i)
  idren (ƛ M)   = cong ƛ (idren M)
  idren (M ∙ N) = cong² _∙_ (idren M) (idren N)


--------------------------------------------------------------------------------
--
-- Substitutions

data _⊢⋆_ : 𝒞 → 𝒞 → Set where
  []    : ∀ {Γ} →
            Γ ⊢⋆ []
  [_,_] : ∀ {Γ Δ A} →
            (xs : Δ ⊢⋆ Γ) (x : Δ ⊢ A) →
            Δ ⊢⋆ [ Γ , A ]

putₛ : ∀ {Γ Δ} → (∀ {A} → Γ ⊢ A → Δ ⊢ A) → Δ ⊢⋆ Γ
putₛ {[]}        f = []
putₛ {[ Γ , A ]} f = [ putₛ (λ M → f (wk M)) , f (ν zero) ]

getₛ : ∀ {Γ Δ A} → Δ ⊢⋆ Γ → Γ ∋ A → Δ ⊢ A
getₛ [ xs , x ] zero    = x
getₛ [ xs , x ] (suc i) = getₛ xs i

unwkₛ : ∀ {Γ Δ A} → Δ ⊢⋆ [ Γ , A ] → Δ ⊢⋆ Γ
unwkₛ [ xs , x ] = xs

wkₛ : ∀ {A Γ Δ} → Δ ⊢⋆ Γ → [ Δ , A ] ⊢⋆ Γ
wkₛ []         = []
wkₛ [ xs , x ] = [ wkₛ xs , wk x ]

liftₛ : ∀ {A Γ Δ} → Δ ⊢⋆ Γ → [ Δ , A ] ⊢⋆ [ Γ , A ]
liftₛ xs = [ wkₛ xs , ν zero ]

idₛ : ∀ {Γ} → Γ ⊢⋆ Γ
idₛ {[]}        = []
idₛ {[ Γ , A ]} = liftₛ idₛ

sub : ∀ {Γ Δ A} → Δ ⊢⋆ Γ → Γ ⊢ A → Δ ⊢ A
sub xs (ν i)   = getₛ xs i
sub xs (ƛ M)   = ƛ (sub (liftₛ xs) M)
sub xs (M ∙ N) = sub xs M ∙ sub xs N

cut : ∀ {Γ A B} → [ Γ , A ] ⊢ B → Γ ⊢ A → Γ ⊢ B
cut M N = sub [ idₛ , N ] M

-- Composition of substitutions
_●_ : ∀ {Γ Δ Φ} → Φ ⊢⋆ Δ → Δ ⊢⋆ Γ → Φ ⊢⋆ Γ
xs ● []         = []
xs ● [ ys , y ] = [ xs ● ys , sub xs y ]

-- subₛ : ∀ {Γ Δ Ξ} → Δ ⊢⋆ Γ → Γ ⊢⋆ Ξ → Δ ⊢⋆ Ξ
-- subₛ xs []         = []
-- subₛ xs [ ys , y ] = [ subₛ xs ys , sub xs y ]


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

module _ where
  open ≡-Reasoning

  wkgetₛ : ∀ {Γ Δ A C} →
             (xs : Δ ⊢⋆ Γ) (i : Γ ∋ C) →
             getₛ (wkₛ {A} xs) i ≡ wk (getₛ xs i)
  wkgetₛ [ xs , x ] zero    = refl
  wkgetₛ [ xs , x ] (suc i) = wkgetₛ xs i

  idgetₛ : ∀ {Γ A} →
             (i : Γ ∋ A) →
             getₛ idₛ i ≡ ν i
  idgetₛ zero    = refl
  idgetₛ (suc i) = begin
                     getₛ (wkₛ idₛ) i
                   ≡⟨ wkgetₛ idₛ i ⟩
                     wk (getₛ idₛ i)
                   ≡⟨ cong wk (idgetₛ i) ⟩
                     wk (ν i)
                   ≡⟨⟩
                     ν (getᵣ (wkᵣ idᵣ) i)
                   ≡⟨ cong ν (wkgetᵣ idᵣ i) ⟩
                     ν (suc (getᵣ idᵣ i))
                   ≡⟨ cong ν (cong suc (idgetᵣ i)) ⟩
                     ν (suc i)
                   ∎

  idsub : ∀ {Γ A} →
            (M : Γ ⊢ A) →
            sub idₛ M ≡ M
  idsub (ν i)   = idgetₛ i
  idsub (ƛ M)   = cong ƛ (idsub M)
  idsub (M ∙ N) = cong² _∙_ (idsub M) (idsub N)


--------------------------------------------------------------------------------
--
-- Conversion of renamings to substitutions

⌊_⌋ : ∀ {Γ Δ} → Δ ∋⋆ Γ → Δ ⊢⋆ Γ
⌊ [] ⌋         = []
⌊ [ xs , x ] ⌋ = [ ⌊ xs ⌋ , ν x ]

module _ where
  open ≡-Reasoning

  ⌊get⌋ : ∀ {Γ Δ A} →
            (xs : Δ ∋⋆ Γ) (i : Γ ∋ A) →
            getₛ ⌊ xs ⌋ i ≡ ν (getᵣ xs i)
  ⌊get⌋ [ xs , x ] zero    = refl
  ⌊get⌋ [ xs , x ] (suc i) = ⌊get⌋ xs i

  ⌊wk⌋ : ∀ {Γ Δ A} →
           (xs : Δ ∋⋆ Γ) →
           wkₛ {A} ⌊ xs ⌋ ≡ ⌊ wkᵣ xs ⌋
  ⌊wk⌋ []         = refl
  ⌊wk⌋ [ xs , x ] = begin
                      [ wkₛ ⌊ xs ⌋ , ν (getᵣ (wkᵣ idᵣ) x) ]
                    ≡⟨ cong² [_,_] refl (cong ν (wkgetᵣ idᵣ x)) ⟩
                      [ wkₛ ⌊ xs ⌋ , ν (suc (getᵣ idᵣ x)) ]
                    ≡⟨ cong² [_,_] (⌊wk⌋ xs) (cong ν (cong suc (idgetᵣ x))) ⟩
                      [ ⌊ wkᵣ xs ⌋ , ν (suc x) ]
                    ∎

  ⌊lift⌋ : ∀ {Γ Δ A} →
             (xs : Δ ∋⋆ Γ) →
             liftₛ {A} ⌊ xs ⌋ ≡ ⌊ liftᵣ xs ⌋
  ⌊lift⌋ xs = cong² [_,_] (⌊wk⌋ xs) refl

  ⌊id⌋ : ∀ {Γ} →
           idₛ {Γ} ≡ ⌊ idᵣ ⌋
  ⌊id⌋ {[]}        = refl
  ⌊id⌋ {[ Γ , A ]} = begin
                       [ wkₛ idₛ , ν zero ]
                     ≡⟨ cong² [_,_] (cong wkₛ ⌊id⌋) refl ⟩
                       [ wkₛ ⌊ idᵣ ⌋ , ν zero ]
                     ≡⟨ cong² [_,_] (⌊wk⌋ idᵣ) refl ⟩
                       [ ⌊ wkᵣ idᵣ ⌋ , ν zero ]
                     ∎


  ⌊sub⌋ : ∀ {Γ Δ A} →
            (xs : Δ ∋⋆ Γ) (M : Γ ⊢ A) →
            sub ⌊ xs ⌋ M ≡ ren xs M
  ⌊sub⌋ xs (ν i)   = ⌊get⌋ xs i
  ⌊sub⌋ xs (ƛ M)   = begin
                       ƛ (sub (liftₛ ⌊ xs ⌋) M)
                     ≡⟨ cong ƛ (cong² sub (⌊lift⌋ xs) (refl {x = M})) ⟩
                       ƛ (sub ⌊ liftᵣ xs ⌋ M)
                     ≡⟨ cong ƛ (⌊sub⌋ (liftᵣ xs) M) ⟩
                       ƛ (ren (liftᵣ xs) M)
                     ∎
  ⌊sub⌋ xs (M ∙ N) = cong² _∙_ (⌊sub⌋ xs M) (⌊sub⌋ xs N)

-- Composition of substitution and renaming
-- TODO: Rename?
_◐_ : ∀ {Γ Δ Ξ} → Ξ ⊢⋆ Δ → Δ ∋⋆ Γ → Ξ ⊢⋆ Γ
xs ◐ ys = xs ● ⌊ ys ⌋

-- projₛ : ∀ {Γ Δ Ξ} → Ξ ⊢⋆ Δ → Δ ∋⋆ Γ → Ξ ⊢⋆ Γ
-- projₛ xs []         = []
-- projₛ xs [ ys , y ] = [ projₛ xs ys , getₛ xs y ]

-- Composition of renaming and substitution
-- TODO: Rename?
_◑_ : ∀ {Γ Δ Ξ} → Δ ∋⋆ Γ → Γ ⊢⋆ Ξ → Δ ⊢⋆ Ξ
xs ◑ ys = ⌊ xs ⌋ ● ys

-- renₛ : ∀ {Γ Δ Ξ} → Δ ∋⋆ Γ → Γ ⊢⋆ Ξ → Δ ⊢⋆ Ξ
-- renₛ xs []         = []
-- renₛ xs [ ys , y ] = [ renₛ xs ys , ren xs y ]


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

module _ where
  open ≡-Reasoning

  zap○ : ∀ {Γ Δ Φ A} →
           (xs : Φ ∋⋆ Δ) (ys : Δ ∋⋆ Γ) (i : Φ ∋ A) →
           [ xs , i ] ○ wkᵣ ys ≡ xs ○ ys
  zap○ xs []         i = refl
  zap○ xs [ ys , y ] i = cong² [_,_] (zap○ xs ys i) refl

  id₁○ : ∀ {Γ Δ} →
           (xs : Δ ∋⋆ Γ) →
           idᵣ ○ xs ≡ xs
  id₁○ []         = refl
  id₁○ [ xs , x ] = cong² [_,_] (id₁○ xs) (idgetᵣ x)

  id₂○ : ∀ {Γ Δ} →
           (xs : Δ ∋⋆ Γ) →
           xs ○ idᵣ ≡ xs
  id₂○ {[]}        []         = refl
  id₂○ {[ Δ , A ]} [ xs , x ] = begin
                                  [ [ xs , x ] ○ wkᵣ idᵣ , x ]
                                ≡⟨ cong² [_,_] (zap○ xs idᵣ x) refl ⟩
                                  [ xs ○ idᵣ , x ]
                                ≡⟨ cong² [_,_] (id₂○ xs) refl ⟩
                                  [ xs , x ]
                                ∎

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

module _ where
  open ≡-Reasoning

  zap◐ : ∀ {Γ Δ Φ A} →
           (xs : Φ ⊢⋆ Δ) (ys : Δ ∋⋆ Γ) (M : Φ ⊢ A) →
           [ xs , M ] ◐ wkᵣ ys ≡ xs ◐ ys
  zap◐ xs []         M = refl
  zap◐ xs [ ys , y ] M = cong² [_,_] (zap◐ xs ys M) refl

  id₂◐ : ∀ {Γ Δ} →
           (xs : Δ ⊢⋆ Γ) →
           xs ◐ idᵣ ≡ xs
  id₂◐ []         = refl
  id₂◐ [ xs , x ] = begin
                      [ [ xs , x ] ◐ wkᵣ idᵣ , x ]
                    ≡⟨ cong² [_,_] (zap◐ xs idᵣ x) refl ⟩
                      [ xs ◐ idᵣ , x ]
                    ≡⟨ cong² [_,_] (id₂◐ xs) refl ⟩
                      [ xs , x ]
                    ∎

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

module _ where
  open ≡-Reasoning

  get○ : ∀ {Γ Δ Φ A} →
           (xs : Φ ∋⋆ Γ) (ys : Γ ∋⋆ Δ) (i : Δ ∋ A) →
           getᵣ (xs ○ ys) i ≡ (getᵣ xs ∘ getᵣ ys) i
  get○ xs [ ys , y ] zero    = refl
  get○ xs [ ys , y ] (suc i) = get○ xs ys i

  assoc○ : ∀ {Γ Δ Φ Ψ} →
             (xs : Ψ ∋⋆ Φ) (ys : Φ ∋⋆ Δ) (zs : Δ ∋⋆ Γ) →
             xs ○ (ys ○ zs) ≡ (xs ○ ys) ○ zs
  assoc○ xs ys []         = refl
  assoc○ xs ys [ zs , z ] = cong² [_,_] (assoc○ xs ys zs) (sym (get○ xs ys z))

  wk○ : ∀ {Γ Δ Φ A} →
          (xs : Φ ∋⋆ Δ) (ys : Δ ∋⋆ Γ) →
          wkᵣ {A} (xs ○ ys) ≡ wkᵣ xs ○ ys
  wk○ xs []         = refl
  wk○ xs [ ys , y ] = cong² [_,_] (wk○ xs ys) (sym (wkgetᵣ xs y))

  lift○ : ∀ {Γ Δ Φ A} →
            (xs : Φ ∋⋆ Δ) (ys : Δ ∋⋆ Γ) →
            liftᵣ {A} (xs ○ ys) ≡ liftᵣ xs ○ liftᵣ ys
  lift○ xs ys = begin
                  liftᵣ (xs ○ ys)
                ≡⟨ cong² [_,_] (wk○ xs ys) refl ⟩
                  [ wkᵣ xs ○ ys , zero ]
                ≡⟨ cong² [_,_] (sym (zap○ (wkᵣ xs) ys zero)) refl ⟩
                  [ [ wkᵣ xs , zero ] ○ wkᵣ ys , zero ]
                ∎

  ren○ : ∀ {Γ Δ Φ A} →
           (xs : Φ ∋⋆ Δ) (ys : Δ ∋⋆ Γ) (M : Γ ⊢ A) →
           ren (xs ○ ys) M ≡ (ren xs ∘ ren ys) M
  ren○ xs ys (ν i)   = cong ν (get○ xs ys i)
  ren○ xs ys (ƛ M)   = begin
                         ƛ (ren (liftᵣ (xs ○ ys)) M)
                       ≡⟨ cong ƛ (cong² ren (lift○ xs ys) refl) ⟩
                         ƛ (ren (liftᵣ xs ○ liftᵣ ys) M)
                       ≡⟨ cong ƛ (ren○ (liftᵣ xs) (liftᵣ ys) M) ⟩
                         ƛ (ren (liftᵣ xs) (ren (liftᵣ ys) M))
                       ∎
  ren○ xs ys (M ∙ N) = cong² _∙_ (ren○ xs ys M) (ren○ xs ys N)

module _ where
  open ≡-Reasoning

  wkid₁○ : ∀ {Γ Δ A} →
             (xs : Δ ∋⋆ Γ) →
             wkᵣ {A} idᵣ ○ xs ≡ wkᵣ xs
  wkid₁○ xs = begin
                wkᵣ idᵣ ○ xs
              ≡⟨ sym (wk○ idᵣ xs) ⟩
                wkᵣ (idᵣ ○ xs)
              ≡⟨ cong wkᵣ (id₁○ xs) ⟩
                wkᵣ xs
              ∎

  wkid₂○ : ∀ {Γ Δ A} →
             (xs : Δ ∋⋆ Γ) →
             wkᵣ {A} xs ○ idᵣ ≡ wkᵣ xs
  wkid₂○ xs = begin
                wkᵣ xs ○ idᵣ
              ≡⟨ sym (wk○ xs idᵣ) ⟩
                wkᵣ (xs ○ idᵣ)
              ≡⟨ cong wkᵣ (id₂○ xs) ⟩
                wkᵣ xs
              ∎

  liftwkid₂○ : ∀ {Γ Δ A} →
                 (xs : Δ ∋⋆ Γ) →
                 liftᵣ {A} xs ○ wkᵣ idᵣ ≡ wkᵣ xs
  liftwkid₂○ xs = begin
                    [ wkᵣ xs , zero ] ○ wkᵣ idᵣ
                  ≡⟨ zap○ (wkᵣ xs) idᵣ zero ⟩
                    wkᵣ xs ○ idᵣ
                  ≡⟨ wkid₂○ xs ⟩
                    wkᵣ xs
                  ∎

  renlift○ : ∀ {Γ Δ Φ A C} →
               (xs : Φ ∋⋆ Δ) (ys : Δ ∋⋆ Γ) (M : [ Γ , A ] ⊢ C) →
               ren (liftᵣ (xs ○ ys)) M ≡ (ren (liftᵣ xs) ∘ ren (liftᵣ ys)) M
  renlift○ xs ys M = begin
                       ren (liftᵣ (xs ○ ys)) M
                     ≡⟨ cong² ren (lift○ xs ys) (refl {x = M}) ⟩
                       ren (liftᵣ xs ○ liftᵣ ys) M
                     ≡⟨ ren○ (liftᵣ xs) (liftᵣ ys) M ⟩
                       (ren (liftᵣ xs) ∘ ren (liftᵣ ys)) M
                     ∎

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

module _ where
  open ≡-Reasoning

  get◐ : ∀ {Γ Δ Φ A} →
           (xs : Φ ⊢⋆ Δ) (ys : Δ ∋⋆ Γ) (i : Γ ∋ A) →
           getₛ (xs ◐ ys) i ≡ (getₛ xs ∘ getᵣ ys) i
  get◐ xs [ ys , y ] zero    = refl
  get◐ xs [ ys , y ] (suc i) = get◐ xs ys i

  assoc◐ : ∀ {Γ Δ Φ Ψ} →
             (xs : Ψ ⊢⋆ Φ) (ys : Φ ∋⋆ Δ) (zs : Δ ∋⋆ Γ) →
             xs ◐ (ys ○ zs) ≡ (xs ◐ ys) ◐ zs
  assoc◐ xs ys []         = refl
  assoc◐ xs ys [ zs , z ] = cong² [_,_] (assoc◐ xs ys zs) (sym (get◐ xs ys z))

  wk◐ : ∀ {Γ Δ Φ A} →
          (xs : Φ ⊢⋆ Δ) (ys : Δ ∋⋆ Γ) →
          wkₛ {A} (xs ◐ ys) ≡ wkₛ xs ◐ ys
  wk◐ xs []         = refl
  wk◐ xs [ ys , y ] = cong² [_,_] (wk◐ xs ys) (sym (wkgetₛ xs y))

  lift◐ : ∀ {Γ Δ Φ A} →
            (xs : Φ ⊢⋆ Δ) (ys : Δ ∋⋆ Γ) →
            liftₛ {A} (xs ◐ ys) ≡ liftₛ xs ◐ liftᵣ ys
  lift◐ xs ys = begin
                  [ wkₛ (xs ◐ ys) , ν zero ]
                ≡⟨ cong² [_,_] (wk◐ xs ys) refl ⟩
                  [ wkₛ xs ◐ ys , ν zero ]
                ≡⟨ cong² [_,_] (sym (zap◐ (wkₛ xs) ys (ν zero))) refl ⟩
                  [ [ wkₛ xs , ν zero ] ◐ wkᵣ ys , ν zero ]
                ∎

  sub◐ : ∀ {Γ Δ Φ A} →
           (xs : Φ ⊢⋆ Δ) (ys : Δ ∋⋆ Γ) (M : Γ ⊢ A) →
           sub (xs ◐ ys) M ≡ (sub xs ∘ ren ys) M
  sub◐ xs ys (ν i)   = get◐ xs ys i
  sub◐ xs ys (ƛ M)   = begin
                         ƛ (sub (liftₛ (xs ◐ ys)) M)
                       ≡⟨ cong ƛ (cong² sub (lift◐ xs ys) (refl {x = M})) ⟩
                         ƛ (sub (liftₛ xs ◐ liftᵣ ys) M)
                       ≡⟨ cong ƛ (sub◐ (liftₛ xs) (liftᵣ ys) M) ⟩
                         ƛ (sub (liftₛ xs) (ren (liftᵣ ys) M))
                       ∎
  sub◐ xs ys (M ∙ N) = cong² _∙_ (sub◐ xs ys M) (sub◐ xs ys N)

module _ where
  open ≡-Reasoning

  wkid₂◐ : ∀ {Γ Δ A} →
             (xs : Δ ⊢⋆ Γ) →
             wkₛ {A} xs ◐ idᵣ ≡ wkₛ xs
  wkid₂◐ xs = begin
                wkₛ xs ◐ idᵣ
              ≡⟨ sym (wk◐ xs idᵣ) ⟩
                wkₛ (xs ◐ idᵣ)
              ≡⟨ cong wkₛ (id₂◐ xs) ⟩
                wkₛ xs
              ∎

  liftwkid₂◐ : ∀ {Γ Δ A} →
                 (xs : Δ ⊢⋆ Γ) →
                 liftₛ {A} xs ◐ wkᵣ idᵣ ≡ wkₛ xs
  liftwkid₂◐ xs = begin
                    [ wkₛ xs , ν zero ] ◐ wkᵣ idᵣ
                  ≡⟨ zap◐ (wkₛ xs) idᵣ (ν zero) ⟩
                    wkₛ xs ◐ idᵣ
                  ≡⟨ wkid₂◐ xs ⟩
                    wkₛ xs
                  ∎

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

module _ where
  open ≡-Reasoning

  zap◑ : ∀ {Γ Δ Φ A} →
           (xs : Φ ∋⋆ Δ) (ys : Δ ⊢⋆ Γ) (i : Φ ∋ A) →
           [ xs , i ] ◑ wkₛ ys ≡ xs ◑ ys
  zap◑ xs []         i = refl
  zap◑ xs [ ys , y ] i = begin
                           [ [ xs , i ] ◑ wkₛ ys , sub [ ⌊ xs ⌋ , ν i ] (wk y) ]
                         ≡⟨ cong² [_,_] (zap◑ xs ys i) (sym (sub◐ [ ⌊ xs ⌋ , ν i ] (wkᵣ idᵣ) y)) ⟩
                           [ xs ◑ ys , sub ([ ⌊ xs ⌋ , ν i ] ◐ wkᵣ idᵣ) y ]
                         ≡⟨ cong² [_,_] refl (cong² sub (zap◐ ⌊ xs ⌋ idᵣ (ν i)) (refl {x = y})) ⟩
                           [ xs ◑ ys , sub (⌊ xs ⌋ ◐ idᵣ) y ]
                         ≡⟨ cong² [_,_] refl (cong² sub (id₂◐ ⌊ xs ⌋) (refl {x = y})) ⟩
                           [ xs ◑ ys , sub ⌊ xs ⌋ y ]
                         ∎

  id₁◑ : ∀ {Γ Δ} →
           (xs : Δ ⊢⋆ Γ) →
           idᵣ ◑ xs ≡ xs
  id₁◑ []         = refl
  id₁◑ [ xs , x ] = begin
                      [ idᵣ ◑ xs , sub ⌊ idᵣ ⌋ x ]
                    ≡⟨ cong² [_,_] (id₁◑ xs) (cong² sub (sym ⌊id⌋) (refl {x = x})) ⟩
                      [ xs , sub idₛ x ]
                    ≡⟨ cong² [_,_] refl (idsub x) ⟩
                      [ xs , x ]
                    ∎

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

module _ where
  open ≡-Reasoning

  zap● : ∀ {Γ Δ Φ A} →
           (xs : Φ ⊢⋆ Δ) (ys : Δ ⊢⋆ Γ) (M : Φ ⊢ A) →
           [ xs , M ] ● wkₛ ys ≡ xs ● ys
  zap● xs []         M = refl
  zap● xs [ ys , y ] M = begin
                           [ [ xs , M ] ● wkₛ ys , sub [ xs , M ] (wk y) ]
                         ≡⟨ cong² [_,_] (zap● xs ys M) (sym (sub◐ [ xs , M ] (wkᵣ idᵣ) y)) ⟩
                           [ xs ● ys , sub ([ xs , M ] ◐ wkᵣ idᵣ) y ]
                         ≡⟨ cong² [_,_] refl (cong² sub (zap◐ xs idᵣ M) (refl {x = y})) ⟩
                           [ xs ● ys , sub (xs ◐ idᵣ) y ]
                         ≡⟨ cong² [_,_] refl (cong² sub (id₂◐ xs) (refl {x = y})) ⟩
                           [ xs ● ys , sub xs y ]
                         ∎

  id₁● : ∀ {Γ Δ} →
           (xs : Δ ⊢⋆ Γ) →
           idₛ ● xs ≡ xs
  id₁● []         = refl
  id₁● [ xs , x ] = cong² [_,_] (id₁● xs) (idsub x)

  id₂● : ∀ {Γ Δ} →
           (xs : Δ ⊢⋆ Γ) →
           xs ● idₛ ≡ xs
  id₂● xs = begin
              xs ● idₛ
            ≡⟨ cong² _●_ refl ⌊id⌋ ⟩
              xs ◐ idᵣ
            ≡⟨ id₂◐ xs ⟩
              xs
            ∎

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

module _ where
  open ≡-Reasoning

  get◑ : ∀ {Γ Δ Φ A} →
           (xs : Φ ∋⋆ Δ) (ys : Δ ⊢⋆ Γ) (i : Γ ∋ A) →
           getₛ (xs ◑ ys) i ≡ (ren xs ∘ getₛ ys) i
  get◑ xs [ ys , y ] zero    = ⌊sub⌋ xs y
  get◑ xs [ ys , y ] (suc i) = get◑ xs ys i

  assoc◑ : ∀ {Γ Δ Φ Ψ} →
             (xs : Ψ ∋⋆ Φ) (ys : Φ ⊢⋆ Δ) (zs : Δ ∋⋆ Γ) →
             xs ◑ (ys ◐ zs) ≡ (xs ◑ ys) ◐ zs
  assoc◑ xs ys []         = refl
  assoc◑ xs ys [ zs , z ] = begin
                              [ xs ◑ (ys ◐ zs) , sub ⌊ xs ⌋ (sub ys (ν z)) ]
                            ≡⟨ cong² [_,_] (assoc◑ xs ys zs) (⌊sub⌋ xs (getₛ ys z)) ⟩
                              [ (xs ◑ ys) ◐ zs , ren xs (getₛ ys z) ]
                            ≡⟨ cong² [_,_] refl (sym (get◑ xs ys z)) ⟩
                              [ (xs ◑ ys) ◐ zs , getₛ (xs ◑ ys) z ]
                            ∎

  wk◑ : ∀ {Γ Δ Φ A} →
          (xs : Φ ∋⋆ Δ) (ys : Δ ⊢⋆ Γ) →
          wkₛ {A} (xs ◑ ys) ≡ wkᵣ xs ◑ ys
  wk◑ xs []         = refl
  wk◑ xs [ ys , y ] = begin
                        [ wkₛ (xs ◑ ys) , wk (sub ⌊ xs ⌋ y) ]
                      ≡⟨ cong² [_,_] refl (cong² ren refl (⌊sub⌋ xs y)) ⟩
                        [ wkₛ (xs ◑ ys) , wk (ren xs y) ]
                      ≡⟨ cong² [_,_] refl (sym (ren○ (wkᵣ idᵣ) xs y)) ⟩
                        [ wkₛ (xs ◑ ys) , ren (wkᵣ idᵣ ○ xs) y ]
                      ≡⟨ cong² [_,_] refl (cong² ren (sym (wk○ idᵣ xs)) refl) ⟩
                        [ wkₛ (xs ◑ ys) , ren (wkᵣ (idᵣ ○ xs)) y ]
                      ≡⟨ cong² [_,_] refl (cong² ren (cong wkᵣ (id₁○ xs)) refl) ⟩
                        [ wkₛ (xs ◑ ys) , ren (wkᵣ xs) y ]
                      ≡⟨ cong² [_,_] (wk◑ xs ys) (sym (⌊sub⌋ (wkᵣ xs) y)) ⟩
                        [ wkᵣ xs ◑ ys , sub ⌊ wkᵣ xs ⌋ y ]
                      ∎

  lift◑ : ∀ {Γ Δ Φ A} →
            (xs : Φ ∋⋆ Δ) (ys : Δ ⊢⋆ Γ) →
            liftₛ {A} (xs ◑ ys) ≡ liftᵣ xs ◑ liftₛ ys
  lift◑ xs ys = begin
                  [ wkₛ (xs ◑ ys) , ν zero ]
                ≡⟨ cong² [_,_] (wk◑ xs ys) refl ⟩
                  [ wkᵣ xs ◑ ys , ν zero ]
                ≡⟨ cong² [_,_] (sym (zap● ⌊ wkᵣ xs ⌋ ys (ν zero))) refl ⟩
                  [ [ ⌊ wkᵣ xs ⌋ , ν zero ] ● wkₛ ys , ν zero ]
                ∎

  sub◑ : ∀ {Γ Δ Φ A} →
           (xs : Φ ∋⋆ Δ) (ys : Δ ⊢⋆ Γ) (M : Γ ⊢ A) →
           sub (xs ◑ ys) M ≡ (ren xs ∘ sub ys) M
  sub◑ xs ys (ν i)   = get◑ xs ys i
  sub◑ xs ys (ƛ M)   = begin
                         ƛ (sub (liftₛ (xs ◑ ys)) M)
                       ≡⟨ cong ƛ (cong² sub (lift◑ xs ys) (refl {x = M})) ⟩
                         ƛ (sub (liftᵣ xs ◑ liftₛ ys) M)
                       ≡⟨ cong ƛ (sub◑ (liftᵣ xs) (liftₛ ys) M) ⟩
                         ƛ (ren (liftᵣ xs) (sub (liftₛ ys) M))
                       ∎
  sub◑ xs ys (M ∙ N) = cong² _∙_ (sub◑ xs ys M) (sub◑ xs ys N)

  sublift◑ : ∀ {Γ Δ Φ A C} →
               (xs : Φ ∋⋆ Δ) (ys : Δ ⊢⋆ Γ) (M : [ Γ , A ] ⊢ C) →
               sub (liftₛ (xs ◑ ys)) M ≡ (ren (liftᵣ xs) ∘ sub (liftₛ ys)) M
  sublift◑ xs ys M = begin
                       sub (liftₛ (xs ◑ ys)) M
                     ≡⟨ cong² sub (lift◑ xs ys) (refl {x = M}) ⟩
                       sub (liftᵣ xs ◑ liftₛ ys) M
                     ≡⟨ sub◑ (liftᵣ xs) (liftₛ ys) M ⟩
                       (ren (liftᵣ xs) ∘ sub (liftₛ ys)) M
                     ∎

module _ where
  open ≡-Reasoning

  wkid₁◑ : ∀ {Γ Δ A} →
             (xs : Δ ⊢⋆ Γ) →
             wkᵣ {A} idᵣ ◑ xs ≡ wkₛ xs
  wkid₁◑ xs = begin
                wkᵣ idᵣ ◑ xs
              ≡⟨ sym (wk◑ idᵣ xs) ⟩
                wkₛ (idᵣ ◑ xs)
              ≡⟨ cong wkₛ (id₁◑ xs) ⟩
                wkₛ xs
              ∎

  liftwkid₁◑ : ∀ {Γ Δ A} →
                 (xs : Δ ⊢⋆ Γ) →
                 (liftᵣ {A} idᵣ ◑ wkₛ xs) ≡ wkₛ xs
  liftwkid₁◑ xs = begin
                    ([ wkᵣ idᵣ , zero ] ◑ wkₛ xs)
                  ≡⟨ zap◑ (wkᵣ idᵣ) xs zero ⟩
                    wkᵣ idᵣ ◑ xs
                  ≡⟨ wkid₁◑ xs ⟩
                    wkₛ xs
                  ∎

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

module _ where
  open ≡-Reasoning

  get● : ∀ {Γ Δ Φ A} →
           (xs : Φ ⊢⋆ Δ) (ys : Δ ⊢⋆ Γ) (i : Γ ∋ A) →
           getₛ (xs ● ys) i ≡ (sub xs ∘ getₛ ys) i
  get● xs [ ys , y ] zero    = refl
  get● xs [ ys , y ] (suc i) = get● xs ys i

  assoc● : ∀ {Γ Δ Φ Ψ} →
             (xs : Ψ ⊢⋆ Φ) (ys : Φ ⊢⋆ Δ) (zs : Δ ∋⋆ Γ) →
             xs ● (ys ◐ zs) ≡ (xs ● ys) ◐ zs
  assoc● xs ys []         = refl
  assoc● xs ys [ zs , z ] = cong² [_,_] (assoc● xs ys zs) (sym (get● xs ys z))

  wk● : ∀ {Γ Δ Φ A} →
          (xs : Φ ⊢⋆ Δ) (ys : Δ ⊢⋆ Γ) →
          wkₛ {A} (xs ● ys) ≡ wkₛ xs ● ys
  wk● xs []         = refl
  wk● xs [ ys , y ] = begin
                        [ wkₛ (xs ● ys) , wk (sub xs y) ]
                      ≡⟨ cong² [_,_] refl (sym (sub◑ (wkᵣ idᵣ) xs y)) ⟩
                        [ wkₛ (xs ● ys) , sub (wkᵣ idᵣ ◑ xs) y ]
                      ≡⟨ cong² [_,_] refl (cong² sub (sym (wk◑ idᵣ xs)) (refl {x = y})) ⟩
                        [ wkₛ (xs ● ys) , sub (wkₛ (idᵣ ◑ xs)) y ]
                      ≡⟨ cong² [_,_] (wk● xs ys) (cong² sub (cong wkₛ (cong² _●_ (sym ⌊id⌋) refl)) (refl {x = y})) ⟩
                        [ wkₛ xs ● ys , sub (wkₛ (idₛ ● xs)) y ]
                      ≡⟨ cong² [_,_] refl (cong² sub (cong wkₛ (id₁● xs)) (refl {x = y})) ⟩
                        [ wkₛ xs ● ys , sub (wkₛ xs) y ]
                      ∎

  lift● : ∀ {Γ Δ Φ A} →
            (xs : Φ ⊢⋆ Δ) (ys : Δ ⊢⋆ Γ) →
            liftₛ {A} (xs ● ys) ≡ liftₛ xs ● liftₛ ys
  lift● xs ys = begin
                  [ wkₛ (xs ● ys) , ν zero ]
                ≡⟨ cong² [_,_] (wk● xs ys) refl ⟩
                  [ wkₛ xs ● ys , ν zero ]
                ≡⟨ cong² [_,_] (sym (zap● (wkₛ xs) ys (ν zero))) refl ⟩
                  [ [ wkₛ xs , ν zero ] ● wkₛ ys , ν zero ]
                ∎

  sub● : ∀ {Γ Δ Φ A} →
           (xs : Φ ⊢⋆ Δ) (ys : Δ ⊢⋆ Γ) (M : Γ ⊢ A) →
           sub (xs ● ys) M ≡ (sub xs ∘ sub ys) M
  sub● xs ys (ν i)   = get● xs ys i
  sub● xs ys (ƛ M)   = begin
                         ƛ (sub (liftₛ (xs ● ys)) M)
                       ≡⟨ cong ƛ (cong² sub (lift● xs ys) (refl {x = M})) ⟩
                         ƛ (sub (liftₛ xs ● liftₛ ys) M)
                       ≡⟨ cong ƛ (sub● (liftₛ xs) (liftₛ ys) M) ⟩
                         ƛ (sub (liftₛ xs) (sub (liftₛ ys) M))
                       ∎
  sub● xs ys (M ∙ N) = cong² _∙_ (sub● xs ys M) (sub● xs ys N)

module _ where
  open ≡-Reasoning

  wkid₁● : ∀ {Γ Δ A} →
             (xs : Δ ⊢⋆ Γ) →
             wkₛ {A} idₛ ● xs ≡ wkₛ xs
  wkid₁● xs = begin
                wkₛ idₛ ● xs
              ≡⟨ sym (wk● idₛ xs) ⟩
                wkₛ (idₛ ● xs)
              ≡⟨ cong wkₛ (id₁● xs) ⟩
                wkₛ xs
              ∎

  wkid₂● : ∀ {Γ Δ A} →
             (xs : Δ ⊢⋆ Γ) →
             wkₛ {A} xs ● idₛ ≡ wkₛ xs
  wkid₂● xs = begin
                wkₛ xs ● idₛ
              ≡⟨ sym (wk● xs idₛ) ⟩
                wkₛ (xs ● idₛ)
              ≡⟨ cong wkₛ (id₂● xs) ⟩
                wkₛ xs
              ∎

  liftwkid₂● : ∀ {Γ Δ A} →
                 (xs : Δ ⊢⋆ Γ) →
                 liftₛ {A} xs ● wkₛ idₛ ≡ wkₛ xs
  liftwkid₂● xs = begin
                    [ wkₛ xs , ν zero ] ● wkₛ idₛ
                  ≡⟨ zap● (wkₛ xs) idₛ (ν zero) ⟩
                    wkₛ xs ● idₛ
                  ≡⟨ wkid₂● xs ⟩
                    wkₛ xs
                  ∎

  sublift● : ∀ {Γ Δ Φ A C} →
               (xs : Φ ⊢⋆ Δ) (ys : Δ ⊢⋆ Γ) (M : [ Γ , A ] ⊢ C) →
               sub (liftₛ (xs ● ys)) M ≡ (sub (liftₛ xs) ∘ sub (liftₛ ys)) M
  sublift● xs ys M = begin
                       sub (liftₛ (xs ● ys)) M
                     ≡⟨ cong² sub (lift● xs ys) (refl {x = M}) ⟩
                       sub (liftₛ xs ● liftₛ ys) M
                     ≡⟨ sub● (liftₛ xs) (liftₛ ys) M ⟩
                       (sub (liftₛ xs) ∘ sub (liftₛ ys)) M
                     ∎

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

module _ where
  open ≡-Reasoning

  renliftwk : ∀ {Γ Δ A C} →
                (xs : Δ ∋⋆ Γ) (M : Γ ⊢ C) →
                ren (liftᵣ xs) (wk {A} M) ≡ ren (wkᵣ xs) M
  renliftwk xs M = begin
                     ren (liftᵣ xs) (wk M)
                   ≡⟨ sym (ren○ (liftᵣ xs) (wkᵣ idᵣ) M) ⟩
                     ren (liftᵣ xs ○ wkᵣ idᵣ) M
                   ≡⟨ cong² ren (zap○ (wkᵣ xs) idᵣ zero) (refl {x = M}) ⟩
                     ren (wkᵣ xs ○ idᵣ) M
                   ≡⟨ cong² ren (id₂○ (wkᵣ xs)) (refl {x = M}) ⟩
                     ren (wkᵣ xs) M
                   ∎

  subliftwk : ∀ {Γ Δ A C} →
                (xs : Δ ⊢⋆ Γ) (M : Γ ⊢ C) →
                sub (liftₛ xs) (wk {A} M) ≡ sub (wkₛ xs) M
  subliftwk xs M = begin
                     sub (liftₛ xs) (wk M)
                   ≡⟨ sym (sub◐ (liftₛ xs) (wkᵣ idᵣ) M) ⟩
                     sub (liftₛ xs ◐ wkᵣ idᵣ) M
                   ≡⟨ cong² sub (zap◐ (wkₛ xs) idᵣ (ν zero)) (refl {x = M}) ⟩
                     sub (wkₛ xs ◐ idᵣ) M
                   ≡⟨ cong² sub (id₂◐ (wkₛ xs)) (refl {x = M}) ⟩
                     sub (wkₛ xs) M
                   ∎


--------------------------------------------------------------------------------
--
-- Convertibility

infix 3 _≅_
data _≅_ : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A → Set where
  refl≅  : ∀ {Γ A} {M : Γ ⊢ A} →
             M ≅ M
  sym≅   : ∀ {Γ A} {M M′ : Γ ⊢ A} →
             M ≅ M′ →
             M′ ≅ M
  trans≅ : ∀ {Γ A} {M M′ M″ : Γ ⊢ A} →
             M ≅ M′ → M′ ≅ M″ →
             M ≅ M″
  congƛ≅ : ∀ {Γ A B} {M M′ : [ Γ , A ] ⊢ B} →
             M ≅ M′ →
             ƛ M ≅ ƛ M′
  cong∙≅ : ∀ {Γ A B} {M M′ : Γ ⊢ A ⊃ B} {N N′ : Γ ⊢ A} →
             M ≅ M′ → N ≅ N′ →
             M ∙ N ≅ M′ ∙ N′
  redβ≅  : ∀ {Γ Δ A B} →
             (xs : Δ ⊢⋆ Γ) (M : [ Γ , A ] ⊢ B) (N : Δ ⊢ A) →
             sub xs (ƛ M) ∙ N ≅ sub [ xs , N ] M
  expη≅  : ∀ {Γ A B} →
             (M : Γ ⊢ A ⊃ B) →
             M ≅ ƛ (wk M ∙ ν zero)

≡→≅ : ∀ {Γ A} {M M′ : Γ ⊢ A} → M ≡ M′ → M ≅ M′
≡→≅ refl = refl≅

module ≅-Reasoning where
  infix 1 begin_
  begin_ : ∀ {Γ A} {M M′ : Γ ⊢ A} → M ≅ M′ → M ≅ M′
  begin p = p

  infixr 2 _≅⟨⟩_
  _≅⟨⟩_ : ∀ {Γ A} (M {M′} : Γ ⊢ A) → M ≅ M′ → M ≅ M′
  M ≅⟨⟩ p = p

  infixr 2 _≅⟨_⟩_
  _≅⟨_⟩_ : ∀ {Γ A} (M {M′ M″} : Γ ⊢ A) → M ≅ M′ → M′ ≅ M″ → M ≅ M″
  M ≅⟨ p ⟩ q = trans≅ p q

  infixr 2 _≡⟨⟩_
  _≡⟨⟩_ : ∀ {Γ A} (M {M′} : Γ ⊢ A) → M ≅ M′ → M ≅ M′
  M ≡⟨⟩ p = p

  infixr 2 _≡⟨_⟩_
  _≡⟨_⟩_ : ∀ {Γ A} (M {M′ M″} : Γ ⊢ A) → M ≡ M′ → M′ ≅ M″ → M ≅ M″
  M ≡⟨ p ⟩ q = trans≅ (≡→≅ p) q

  infix 3 _∎
  _∎ : ∀ {Γ A} (M : Γ ⊢ A) → M ≅ M
  M ∎ = refl≅


--------------------------------------------------------------------------------
--
-- Convertibility of substitutions

infix 3 _≅⋆_
data _≅⋆_ : ∀ {Γ Δ} → Δ ⊢⋆ Γ → Δ ⊢⋆ Γ → Set where
  []    : ∀ {Δ} →
            ([] {Δ}) ≅⋆ ([] {Δ})
  [_,_] : ∀ {Γ Δ A} {xs xs′ : Δ ⊢⋆ Γ} {M M′ : Δ ⊢ A} →
            (ps : xs ≅⋆ xs′) (p : M ≅ M′) →
            [ xs , M ] ≅⋆ [ xs′ , M′ ]

refl≅⋆ : ∀ {Γ Δ} {xs : Δ ⊢⋆ Γ} → xs ≅⋆ xs
refl≅⋆ {xs = []}         = []
refl≅⋆ {xs = [ xs , x ]} = [ refl≅⋆ , refl≅ ]

sym≅⋆ : ∀ {Γ Δ} {xs xs′ : Δ ⊢⋆ Γ} → xs ≅⋆ xs′ → xs′ ≅⋆ xs
sym≅⋆ []         = []
sym≅⋆ [ ps , p ] = [ sym≅⋆ ps , sym≅ p ]

trans≅⋆ : ∀ {Γ Δ} {xs xs′ xs″ : Δ ⊢⋆ Γ} → xs ≅⋆ xs′ → xs′ ≅⋆ xs″ → xs ≅⋆ xs″
trans≅⋆ []         []         = []
trans≅⋆ [ ps , p ] [ qs , q ] = [ trans≅⋆ ps qs , trans≅ p q ]

≡→≅⋆ : ∀ {Γ Δ} {xs xs′ : Δ ⊢⋆ Γ} → xs ≡ xs′ → xs ≅⋆ xs′
≡→≅⋆ refl = refl≅⋆

module ≅⋆-Reasoning where
  infix 1 begin_
  begin_ : ∀ {Γ Δ} {xs xs′ : Δ ⊢⋆ Γ} → xs ≅⋆ xs′ → xs ≅⋆ xs′
  begin ps = ps

  infixr 2 _≅⋆⟨⟩_
  _≅⋆⟨⟩_ : ∀ {Γ Δ} (xs {xs′} : Δ ⊢⋆ Γ) → xs ≅⋆ xs′ → xs ≅⋆ xs′
  xs ≅⋆⟨⟩ ps = ps

  infixr 2 _≅⋆⟨_⟩_
  _≅⋆⟨_⟩_ : ∀ {Γ Δ} (xs {xs′ xs″} : Δ ⊢⋆ Γ) → xs ≅⋆ xs′ → xs′ ≅⋆ xs″ → xs ≅⋆ xs″
  xs ≅⋆⟨ ps ⟩ qs = trans≅⋆ ps qs

  infixr 2 _≡⟨⟩_
  _≡⟨⟩_ : ∀ {Γ Δ} (xs {xs′} : Δ ⊢⋆ Γ) → xs ≅⋆ xs′ → xs ≅⋆ xs′
  xs ≡⟨⟩ ps = ps

  infixr 2 _≡⟨_⟩_
  _≡⟨_⟩_ : ∀ {Γ Δ} (xs {xs′ xs″} : Δ ⊢⋆ Γ) → xs ≡ xs′ → xs′ ≅⋆ xs″ → xs ≅⋆ xs″
  xs ≡⟨ ps ⟩ qs = trans≅⋆ (≡→≅⋆ ps) qs

  infix 3 _∎
  _∎ : ∀ {Γ Δ} (xs : Δ ⊢⋆ Γ) → xs ≅⋆ xs
  xs ∎ = refl≅⋆


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

module _ where
  open ≅-Reasoning

  congrenβ≅ : ∀ {Γ Δ Φ A B} {xs : Φ ∋⋆ Δ} →
                (ys : Δ ⊢⋆ Γ) (M : [ Γ , A ] ⊢ B) (N : Δ ⊢ A) →
                ren xs (sub ys (ƛ M) ∙ N) ≅ ren xs (sub [ ys , N ] M)
  congrenβ≅ {xs = xs} ys M N =
    begin
      ƛ (ren (liftᵣ xs) (sub (liftₛ ys) M)) ∙ ren xs N
    ≅⟨ cong∙≅ (congƛ≅ (≡→≅ (sym (sublift◑ xs ys M)))) refl≅ ⟩
      sub (xs ◑ ys) (ƛ M) ∙ ren xs N
    ≅⟨ redβ≅ (xs ◑ ys) M (ren xs N) ⟩
      sub [ xs ◑ ys , ren xs N ] M
    ≡⟨ cong² sub (cong² [_,_] refl (sym (⌊sub⌋ xs N))) (refl {x = M}) ⟩
      sub (xs ◑ [ ys , N ]) M
    ≡⟨ sub◑ xs [ ys , N ] M ⟩
      ren xs (sub [ ys , N ] M)
    ∎

  congrenην≅ : ∀ {Γ Δ A B} {xs : Δ ∋⋆ Γ} →
                 (i : Γ ∋ A ⊃ B) →
                 ren xs (ν i) ≅ ren xs (ƛ (wk (ν i) ∙ ν zero))
  congrenην≅ {xs = xs} i =
    begin
      ν (getᵣ xs i)
    ≅⟨ expη≅ (ν (getᵣ xs i)) ⟩
      ƛ (wk (ν (getᵣ xs i)) ∙ ν zero)
    ≅⟨ congƛ≅ (cong∙≅ (≡→≅ (cong ν (sym (get○ (wkᵣ idᵣ) xs i)))) refl≅) ⟩
      ƛ (ν (getᵣ (wkᵣ idᵣ ○ xs) i) ∙ ν zero)
    ≅⟨ congƛ≅ (cong∙≅ (≡→≅ (cong ν (cong² getᵣ (wkid₁○ xs) (refl {x = i})))) refl≅) ⟩
      ƛ (ν (getᵣ (wkᵣ xs) i) ∙ ν zero)
    ≅⟨ congƛ≅ (cong∙≅ (≡→≅ (cong ν (cong² getᵣ (sym (liftwkid₂○ xs)) (refl {x = i})))) refl≅) ⟩
      ƛ (ν (getᵣ (liftᵣ xs ○ wkᵣ idᵣ) i) ∙ ν zero)
    ≅⟨ congƛ≅ (cong∙≅ (≡→≅ (cong ν (get○ (liftᵣ xs) (wkᵣ idᵣ) i))) refl≅) ⟩
      ƛ (ν (getᵣ (liftᵣ xs) (getᵣ (wkᵣ idᵣ) i)) ∙ ν zero)
    ∎

  congrenηƛ≅ : ∀ {Γ Δ A B} {xs : Δ ∋⋆ Γ} →
                 (M : [ Γ , A ] ⊢ B) →
                 ren xs (ƛ M) ≅ ren xs (ƛ (wk (ƛ M) ∙ ν zero))
  congrenηƛ≅ {xs = xs} M =
    begin
      ƛ (ren (liftᵣ xs) M)
    ≅⟨ expη≅ (ƛ (ren (liftᵣ xs) M))  ⟩
      ƛ (wk (ƛ (ren (liftᵣ xs) M)) ∙ ν zero)
    ≡⟨⟩
      ƛ (ƛ (ren (liftᵣ (wkᵣ idᵣ)) (ren (liftᵣ xs) M)) ∙ ν zero)
    ≅⟨ congƛ≅ (cong∙≅ (congƛ≅ (≡→≅ (sym (renlift○ (wkᵣ idᵣ) xs M)))) refl≅) ⟩
      ƛ (ƛ (ren (liftᵣ (wkᵣ idᵣ ○ xs)) M) ∙ ν zero)
    ≅⟨ congƛ≅ (cong∙≅ (congƛ≅ (≡→≅ (cong² ren (cong liftᵣ (wkid₁○ xs)) (refl {x = M})))) refl≅) ⟩
      ƛ (ƛ (ren (liftᵣ (wkᵣ xs)) M) ∙ ν zero)
    ≅⟨ congƛ≅ (cong∙≅ (congƛ≅ (≡→≅ (cong² ren (cong liftᵣ (sym (wkid₂○ xs))) (refl {x = M})))) refl≅) ⟩
      ƛ (ƛ (ren (liftᵣ (wkᵣ xs ○ idᵣ)) M) ∙ ν zero)
    ≅⟨ congƛ≅ (cong∙≅ (congƛ≅ (≡→≅ (cong² ren (cong liftᵣ (sym (zap○ (wkᵣ xs) idᵣ zero))) (refl {x = M})))) refl≅) ⟩
      ƛ (ƛ (ren (liftᵣ ([ wkᵣ xs , zero ] ○ wkᵣ idᵣ)) M) ∙ ν zero)
    ≅⟨ congƛ≅ (cong∙≅ (congƛ≅ (≡→≅ (renlift○ [ wkᵣ xs , zero ] (wkᵣ idᵣ) M))) refl≅) ⟩
      ƛ (ƛ (ren (liftᵣ (liftᵣ xs)) (ren (liftᵣ (wkᵣ idᵣ)) M)) ∙ ν zero)
    ∎

  congrenη∙≅ : ∀ {Γ Δ A B C} {xs : Δ ∋⋆ Γ} →
                 (M : Γ ⊢ C ⊃ B ⊃ A) (N : Γ ⊢ C) →
                 ren xs (M ∙ N) ≅ ren xs (ƛ (wk (M ∙ N) ∙ ν zero))
  congrenη∙≅ {xs = xs} M N =
    begin
      ren xs M ∙ ren xs N
    ≅⟨ expη≅ (ren xs M ∙ ren xs N) ⟩
      ƛ (wk (ren xs M ∙ ren xs N) ∙ ν zero)
    ≡⟨⟩
      ƛ ((ren (wkᵣ idᵣ) (ren xs M) ∙ ren (wkᵣ idᵣ) (ren xs N)) ∙ ν zero)
    ≅⟨ congƛ≅ (cong∙≅ (cong∙≅ (≡→≅ (sym (ren○ (wkᵣ idᵣ) xs M))) (≡→≅ (sym (ren○ (wkᵣ idᵣ) xs N)))) refl≅) ⟩
      ƛ ((ren (wkᵣ idᵣ ○ xs) M ∙ ren (wkᵣ idᵣ ○ xs) N) ∙ ν zero)
    ≅⟨ congƛ≅ (cong∙≅ (cong∙≅ (≡→≅ (cong² ren (wkid₁○ xs) (refl {x = M}))) (≡→≅ (cong² ren (wkid₁○ xs) (refl {x = N})))) refl≅) ⟩
      ƛ ((ren (wkᵣ xs) M ∙ ren (wkᵣ xs) N) ∙ ν zero)
    ≅⟨ congƛ≅ (cong∙≅ (cong∙≅ (≡→≅ (cong² ren (sym (wkid₂○ xs)) (refl {x = M}))) (≡→≅ (cong² ren (sym (wkid₂○ xs)) (refl {x = N})))) refl≅) ⟩
      ƛ ((ren (wkᵣ xs ○ idᵣ) M ∙ ren (wkᵣ xs ○ idᵣ) N) ∙ ν zero)
    ≅⟨ congƛ≅ (cong∙≅ (cong∙≅ (≡→≅ (cong² ren (wkid₂○ xs) (refl {x = M}))) (≡→≅ (cong² ren (wkid₂○ xs) (refl {x = N})))) refl≅) ⟩
      ƛ ((ren (wkᵣ xs) M ∙ ren (wkᵣ xs) N) ∙ ν zero)
    ≅⟨ congƛ≅ (cong∙≅ (cong∙≅ (≡→≅ (sym (renliftwk xs M))) (≡→≅ (sym (renliftwk xs N)))) refl≅) ⟩
      ƛ ((ren (liftᵣ xs) (wk M) ∙ ren (liftᵣ xs) (wk N)) ∙ ν zero)
    ∎

  congren≅ : ∀ {Γ Δ A} {xs : Δ ∋⋆ Γ} {M M′ : Γ ⊢ A} →
               M ≅ M′ →
               ren xs M ≅ ren xs M′
  congren≅ refl≅           = refl≅
  congren≅ (sym≅ p)        = sym≅ (congren≅ p)
  congren≅ (trans≅ p q)    = trans≅ (congren≅ p) (congren≅ q)
  congren≅ (congƛ≅ p)      = congƛ≅ (congren≅ p)
  congren≅ (cong∙≅ p q)    = cong∙≅ (congren≅ p) (congren≅ q)
  congren≅ (redβ≅ xs M N)  = congrenβ≅ xs M N
  congren≅ (expη≅ (ν i))   = congrenην≅ i
  congren≅ (expη≅ (ƛ M))   = congrenηƛ≅ M
  congren≅ (expη≅ (M ∙ N)) = congrenη∙≅ M N

  congwk≅ : ∀ {Γ A C} {M M′ : Γ ⊢ C} →
              M ≅ M′ →
              wk {A} M ≅ wk M′
  congwk≅ p = congren≅ p


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

congwk≅⋆ : ∀ {Γ Δ A} {xs xs′ : Δ ⊢⋆ Γ} →
             xs ≅⋆ xs′ →
             wkₛ {A} xs ≅⋆ wkₛ xs′
congwk≅⋆ []         = []
congwk≅⋆ [ ps , p ] = [ congwk≅⋆ ps , congwk≅ p ]

conglift≅⋆ : ∀ {Γ Δ A} {xs xs′ : Δ ⊢⋆ Γ} →
               xs ≅⋆ xs′ →
               liftₛ {A} xs ≅⋆ liftₛ xs′
conglift≅⋆ []         = [ [] , refl≅ ]
conglift≅⋆ [ ps , p ] = [ [ congwk≅⋆ ps , congwk≅ p ] , refl≅ ]


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

module _ where
  open ≅-Reasoning

  congsubβ≅ : ∀ {Γ Δ Φ A B} {xs : Φ ⊢⋆ Δ} →
                (ys : Δ ⊢⋆ Γ) (M : [ Γ , A ] ⊢ B) (N : Δ ⊢ A) →
                sub xs (sub ys (ƛ M) ∙ N) ≅ sub xs (sub [ ys , N ] M)
  congsubβ≅ {xs = xs} ys M N =
    begin
      ƛ (sub (liftₛ xs) (sub (liftₛ ys) M)) ∙ sub xs N
    ≅⟨ cong∙≅ (congƛ≅ (≡→≅ (sym (sublift● xs ys M)))) refl≅ ⟩
      sub (xs ● ys) (ƛ M) ∙ sub xs N
    ≅⟨ redβ≅ (xs ● ys) M (sub xs N) ⟩
      sub [ xs ● ys , sub xs N ] M
    ≡⟨ sub● xs [ ys , N ] M ⟩
      sub xs (sub [ ys , N ] M)
    ∎

  congsubην≅ : ∀ {Γ Δ A B} {xs : Δ ⊢⋆ Γ} →
                 (i : Γ ∋ A ⊃ B) →
                 sub xs (ν i) ≅ sub xs (ƛ (wk (ν i) ∙ ν zero))
  congsubην≅ {xs = xs} i =
    begin
      getₛ xs i
    ≅⟨ expη≅ (getₛ xs i) ⟩
      ƛ (wk (getₛ xs i) ∙ ν zero)
    ≅⟨ congƛ≅ (cong∙≅ (≡→≅ (sym (wkgetₛ xs i))) refl≅) ⟩
      ƛ (getₛ (wkₛ xs) i ∙ ν zero)
    ≅⟨ congƛ≅ (cong∙≅ (≡→≅ (cong² getₛ (sym (liftwkid₂◐ xs)) (refl {x = i}))) refl≅) ⟩
      ƛ (getₛ (liftₛ xs ◐ wkᵣ idᵣ) i ∙ ν zero)
    ≅⟨ congƛ≅ (cong∙≅ (≡→≅ (get◐ (liftₛ xs) (wkᵣ idᵣ) i)) refl≅) ⟩
      ƛ (getₛ (liftₛ xs) (getᵣ (wkᵣ idᵣ) i) ∙ ν zero)
    ∎

  congsubηƛ≅ : ∀ {Γ Δ A B} {xs : Δ ⊢⋆ Γ} →
                 (M : [ Γ , A ] ⊢ B) →
                 sub xs (ƛ M) ≅ sub xs (ƛ (wk (ƛ M) ∙ ν zero))
  congsubηƛ≅ {xs = xs} M =
    begin
      ƛ (sub [ wkₛ xs , ν zero ] M)
    ≅⟨ congƛ≅ (≡→≅ (cong² sub (cong² [_,_] (sym (id₂◐ (wkₛ xs))) refl) (refl {x = M}))) ⟩
      ƛ (sub [ wkₛ xs ◐ idᵣ , ν zero ] M)
    ≅⟨ congƛ≅ (≡→≅ (cong² sub (cong² [_,_] (sym (zap◐ (wkₛ xs) idᵣ (ν zero))) refl) (refl {x = M}))) ⟩
      ƛ (sub [ [ wkₛ xs , ν zero ] ◐ wkᵣ idᵣ , ν zero ] M)
    ≅⟨ congƛ≅ (≡→≅ (cong² sub (cong² [_,_] (sym (zap◐ [ wkₛ xs , ν zero ] (wkᵣ idᵣ) (ν zero))) refl) (refl {x = M}))) ⟩
      ƛ (sub [ [ [ wkₛ xs , ν zero ] , ν zero ] ◐ (wkᵣ (wkᵣ idᵣ)) , ν zero ] M)
    ≡⟨⟩
      ƛ (sub ([ liftₛ xs , ν zero ] ◐ liftᵣ (wkᵣ idᵣ)) M)
    ≅⟨ congƛ≅ (≡→≅ (sub◐ [ liftₛ xs , ν zero ] (liftᵣ (wkᵣ idᵣ)) M)) ⟩
      ƛ (sub [ liftₛ xs , ν zero ] (ren (liftᵣ (wkᵣ idᵣ)) M))
    ≅⟨ congƛ≅ (sym≅ (redβ≅ (liftₛ xs) (ren (liftᵣ (wkᵣ idᵣ)) M) (ν zero))) ⟩
      ƛ (ƛ (sub (liftₛ (liftₛ xs)) (ren (liftᵣ (wkᵣ idᵣ)) M)) ∙ ν zero)
    ∎

  congsubη∙≅ : ∀ {Γ Δ A B C} {xs : Δ ⊢⋆ Γ} →
                 (M : Γ ⊢ C ⊃ A ⊃ B) (N : Γ ⊢ C) →
                 sub xs (M ∙ N) ≅ sub xs (ƛ (wk (M ∙ N) ∙ ν zero))
  congsubη∙≅ {xs = xs} M N =
    begin
      sub xs M ∙ sub xs N
    ≅⟨ expη≅ (sub xs M ∙ sub xs N) ⟩
      ƛ (wk (sub xs M ∙ sub xs N) ∙ ν zero)
    ≅⟨ congƛ≅ (cong∙≅ (cong∙≅ (≡→≅ (sym (sub◑ (wkᵣ idᵣ) xs M))) (≡→≅ (sym (sub◑ (wkᵣ idᵣ) xs N)))) refl≅) ⟩
      ƛ ((sub (wkᵣ idᵣ ◑ xs) M ∙ sub (wkᵣ idᵣ ◑ xs) N) ∙ ν zero)
    ≅⟨ congƛ≅ (cong∙≅ (cong∙≅ (≡→≅ (cong² sub (wkid₁◑ xs) (refl {x = M}))) (≡→≅ (cong² sub (wkid₁◑ xs) (refl {x = N})))) refl≅) ⟩
      ƛ ((sub (wkₛ xs) M ∙ sub (wkₛ xs) N) ∙ ν zero)
    ≅⟨ congƛ≅ (cong∙≅ (cong∙≅ (≡→≅ (sym (subliftwk xs M))) (≡→≅ (sym (subliftwk xs N)))) refl≅) ⟩
      ƛ ((sub (liftₛ xs) (wk M) ∙ sub (liftₛ xs) (wk N)) ∙ ν zero)
    ∎

  congsub≅ : ∀ {Γ Δ A} {xs xs′ : Δ ⊢⋆ Γ} {M M′ : Γ ⊢ A} →
               xs ≅⋆ xs′ → M ≅ M′ →
               sub xs M ≅ sub xs M′
  congsub≅ ps refl≅           = refl≅
  congsub≅ ps (sym≅ p)        = sym≅ (congsub≅ ps p)
  congsub≅ ps (trans≅ p q)    = trans≅ (congsub≅ ps p) (congsub≅ ps q)
  congsub≅ ps (congƛ≅ p)      = congƛ≅ (congsub≅ (conglift≅⋆ ps) p)
  congsub≅ ps (cong∙≅ p q)    = cong∙≅ (congsub≅ ps p) (congsub≅ ps q)
  congsub≅ ps (redβ≅ xs M N)  = congsubβ≅ xs M N
  congsub≅ ps (expη≅ (ν i))   = congsubην≅ i
  congsub≅ ps (expη≅ (ƛ M))   = congsubηƛ≅ M
  congsub≅ ps (expη≅ (M ∙ N)) = congsubη∙≅ M N


--------------------------------------------------------------------------------
--
-- Model

record 𝔐 : Set₁ where
  field
    𝒲      : Set
    𝒢      : 𝒲 → Set
    _⊒_    : 𝒲 → 𝒲 → Set
    id⊒    : ∀ {W} →
               W ⊒ W
    _◇_    : ∀ {U V W} →
               U ⊒ V → V ⊒ W →
               U ⊒ W
    lid◇   : ∀ {V W} →
               (xs : V ⊒ W) →
               id⊒ ◇ xs ≡ xs
    rid◇   : ∀ {V W} →
               (xs : V ⊒ W) →
               xs ◇ id⊒ ≡ xs
    assoc◇ : ∀ {T U V W} →
               (xs : T ⊒ U) (ys : U ⊒ V) (zs : V ⊒ W) →
               xs ◇ (ys ◇ zs) ≡ (xs ◇ ys) ◇ zs


--------------------------------------------------------------------------------
--
-- Semantic objects

module _ {{𝔪 : 𝔐}} where
  open 𝔐 𝔪

  infix 3 _⊩_
  data _⊩_ : 𝒲 → 𝒯 → Set where
    ⟦G⟧ : ∀ {W} →
            (h : ∀ {V} →
                   (xs : V ⊒ W) →
                   𝒢 V) →
            W ⊩ •
    ⟦ƛ⟧ : ∀ {W A B} →
            (h : ∀ {V} →
                   (xs : V ⊒ W) (a : V ⊩ A) →
                   V ⊩ B) →
            W ⊩ A ⊃ B

  ⟦g⟧⟨_⟩ : ∀ {V W} →
             V ⊒ W → W ⊩ • →
             𝒢 V
  ⟦g⟧⟨ xs ⟩ (⟦G⟧ f) = f xs

  _◎⟨_⟩_ : ∀ {V W A B} →
             W ⊩ A ⊃ B → V ⊒ W → V ⊩ A →
             V ⊩ B
  (⟦ƛ⟧ f) ◎⟨ xs ⟩ a = f xs a


  -- Renamings on semantic objects

  -- ⟦putᵣ⟧ can’t be stated here
  -- ⟦getᵣ⟧ can’t be stated here
  -- ⟦unwkᵣ⟧ can’t be stated here
  -- ⟦wkᵣ⟧ can’t be stated here
  -- ⟦liftᵣ⟧ can’t be stated here
  -- ⟦idᵣ⟧ = id⊒

  -- ⟦ren⟧ = acc
  acc : ∀ {A V W} → V ⊒ W → W ⊩ A → V ⊩ A
  acc {•}     xs f = ⟦G⟧ (λ ys   → ⟦g⟧⟨ ys ◇ xs ⟩ f)
  acc {A ⊃ B} xs f = ⟦ƛ⟧ (λ ys a → f ◎⟨ ys ◇ xs ⟩ a)

  -- ⟦wk⟧ can’t be stated here
  -- _⟦○⟧_ = _◇_


--------------------------------------------------------------------------------
--
-- Semantic equality

module _ {{𝔪 : 𝔐}} where
  open 𝔐 𝔪

  mutual
    data Eq : ∀ {A W} → W ⊩ A → W ⊩ A → Set where
      eq• : ∀ {W} {f f′ : W ⊩ •} →
              (h : ∀ {V} →
                     (xs : V ⊒ W) →
                     ⟦g⟧⟨ xs ⟩ f ≡ ⟦g⟧⟨ xs ⟩ f′) →
              Eq f f′
      eq⊃ : ∀ {A B W} {f f′ : W ⊩ A ⊃ B} →
              (h : ∀ {V} →
                     (xs : V ⊒ W) {a : V ⊩ A} (u : Un a) →
                     Eq (f ◎⟨ xs ⟩ a) (f′ ◎⟨ xs ⟩ a)) →
              Eq f f′

    data Un : ∀ {A W} → W ⊩ A → Set where
      un• : ∀ {W} {f : W ⊩ •} →
              Un f
      un⊃ : ∀ {A B W} {f : W ⊩ A ⊃ B} →
              (h₀ : ∀ {V} →
                      (xs : V ⊒ W) {a : V ⊩ A} (u : Un a) →
                      Un (f ◎⟨ xs ⟩ a)) →
              (h₁ : ∀ {V} →
                      (xs : V ⊒ W) {a a′ : V ⊩ A} (e : Eq a a′) (u : Un a) (u′ : Un a′) →
                      Eq (f ◎⟨ xs ⟩ a) (f ◎⟨ xs ⟩ a′)) →
              (h₂ : ∀ {U V} →
                      (xs : U ⊒ V) (ys : V ⊒ W) (zs : U ⊒ W) {a : V ⊩ A} (u : Un a) →
                      Eq (acc xs (f ◎⟨ ys ⟩ a)) (f ◎⟨ zs ⟩ (acc xs a))) →
              Un f

  reflEq : ∀ {A W} {a : W ⊩ A} → Un a → Eq a a
  reflEq un•            = eq• (λ xs   → refl)
  reflEq (un⊃ h₀ h₁ h₂) = eq⊃ (λ xs u → reflEq (h₀ xs u))

  symEq : ∀ {A W} {a a′ : W ⊩ A} → Eq a a′ → Eq a′ a
  symEq {•}     (eq• h) = eq• (λ xs   → sym (h xs))
  symEq {A ⊃ B} (eq⊃ h) = eq⊃ (λ xs u → symEq (h xs u))

  transEq : ∀ {A W} {a a′ a″ : W ⊩ A} → Eq a a′ → Eq a′ a″ → Eq a a″
  transEq {•}     (eq• h) (eq• h′) = eq• (λ xs   → trans (h xs) (h′ xs))
  transEq {A ⊃ B} (eq⊃ h) (eq⊃ h′) = eq⊃ (λ xs u → transEq (h xs u) (h′ xs u))

  ≡→Eq : ∀ {A W} {a a′ : W ⊩ A} → a ≡ a′ → Un a → Eq a a′
  ≡→Eq refl u = reflEq u

  module Eq-Reasoning where
    infix 1 begin_
    begin_ : ∀ {A W} {a a′ : W ⊩ A} → Eq a a′ → Eq a a′
    begin e = e

    infixr 2 _Eq⟨⟩_
    _Eq⟨⟩_ : ∀ {A W} (a {a′} : W ⊩ A) → Eq a a′ → Eq a a′
    a Eq⟨⟩ e = e

    infixr 2 _Eq⟨_⟩_
    _Eq⟨_⟩_ : ∀ {A W} (a {a′ a″} : W ⊩ A) → Eq a a′ → Eq a′ a″ → Eq a a″
    a Eq⟨ e ⟩ e′ = transEq e e′

    infixr 2 _≡⟨⟩_
    _≡⟨⟩_ : ∀ {A W} (a {a′} : W ⊩ A) → Eq a a′ → Eq a a′
    a ≡⟨⟩ e = e

    infixr 2 _≡⟨_∣_⟩_
    _≡⟨_∣_⟩_ : ∀ {A W} (a {a′ a″} : W ⊩ A) → a ≡ a′ → Un a → Eq a′ a″ → Eq a a″
    a ≡⟨ e ∣ u ⟩ e′ = transEq (≡→Eq e u) e′

    infix 3 _∎⟨_⟩
    _∎⟨_⟩ : ∀ {A W} (a : W ⊩ A) → Un a → Eq a a
    a ∎⟨ u ⟩ = reflEq u


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

module _ {{𝔪 : 𝔐}} where
  open 𝔐 𝔪

  -- cong◎⟨_⟩Eq
  postulate
    ◎Eq : ∀ {A B V W} {f f′ : W ⊩ A ⊃ B} {a a′ : V ⊩ A} →
              (xs : V ⊒ W) → Eq f f′ → Un f → Un f′ → Eq a a′ → Un a → Un a′ →
              Eq (f ◎⟨ xs ⟩ a) (f′ ◎⟨ xs ⟩ a′)

  -- cong↑⟨_⟩Eq
  postulate
    accEq : ∀ {A V W} {a a′ : W ⊩ A} →
              (xs : V ⊒ W) → Eq a a′ →
              Eq (acc xs a) (acc xs a′)

  -- cong↑⟨_⟩𝒰
  postulate
    accUn : ∀ {A V W} {a : W ⊩ A} →
              (xs : V ⊒ W) → Un a →
              Un (acc xs a)

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

module _ {{𝔪 : 𝔐}} where
  open 𝔐 𝔪

  -- aux₄₁₁
  postulate
    idaccEq : ∀ {A W} {a : W ⊩ A} →
                Un a →
                Eq (acc id⊒ a) a

  -- aux₄₁₂
  postulate
    accaccEq : ∀ {A U V W} {a : W ⊩ A} →
                 (xs : U ⊒ V) (ys : V ⊒ W) → Un a →
                 Eq (acc xs (acc ys a)) (acc (xs ◇ ys) a)

  -- aux₄₁₃
  postulate
    acc◎Eq : ∀ {A B V W} {f : W ⊩ A ⊃ B} {a : V ⊩ A} →
                 (xs : V ⊒ W) → Un f → Un a →
                 Eq (f ◎⟨ xs ⟩ a) (acc xs f ◎⟨ id⊒ ⟩ a)


--------------------------------------------------------------------------------
--
-- Semantic environments

module _ {{𝔪 : 𝔐}} where
  open 𝔐 𝔪

  infix 3 _⊩⋆_
  data _⊩⋆_ : 𝒲 → 𝒞 → Set where
    []    : ∀ {W} →
              W ⊩⋆ []
    [_,_] : ∀ {Γ A W} →
              (vs : W ⊩⋆ Γ) (v : W ⊩ A) →
              W ⊩⋆ [ Γ , A ]

  -- ⟦putₛ⟧ can’t be stated here

  -- ⟦getₛ⟧ = get ; lookup = get
  get : ∀ {Γ A W} → W ⊩⋆ Γ → Γ ∋ A → W ⊩ A
  get [ vs , v ] zero    = v
  get [ vs , v ] (suc i) = get vs i

  -- ⟦unwkₛ⟧ = unwk
  -- TODO: Unneeded
  -- unwk : ∀ {Γ A W} → W ⊩⋆ [ Γ , A ] → W ⊩⋆ Γ
  -- unwk [ vs , v ] = vs

  -- ⟦wkₛ⟧ can’t be stated here
  -- ⟦liftₛ⟧ can’t be stated here
  -- ⟦idₛ⟧ can’t be stated here
  -- ⟦sub⟧ can’t be stated here
  -- ⟦cut⟧ can’t be stated here
  -- _◆_ can’t be stated here

  -- ⟦_◑_⟧ = acc⋆ ; ↑⟨_⟩⊩⋆ = acc⋆
  acc⋆ : ∀ {Γ V W} → V ⊒ W → W ⊩⋆ Γ → V ⊩⋆ Γ
  acc⋆ xs []         = []
  acc⋆ xs [ vs , v ] = [ acc⋆ xs vs , acc xs v ]

  -- ⟦_◐_⟧ = get⋆ ; ↓⟨_⟩⊩⋆ = flip get⋆
  get⋆ : ∀ {Γ Δ W} → W ⊩⋆ Δ → Δ ∋⋆ Γ → W ⊩⋆ Γ
  get⋆ vs []         = []
  get⋆ vs [ ys , y ] = [ get⋆ vs ys , get vs y ]


--------------------------------------------------------------------------------
--
-- Semantic equality on environments

module _ {{𝔪 : 𝔐}} where
  open 𝔐 𝔪

  data Eq⋆ : ∀ {Γ W} → W ⊩⋆ Γ → W ⊩⋆ Γ → Set where
    []    : ∀ {W} →
              Eq⋆ ([] {W}) ([] {W})
    [_,_] : ∀ {Γ A W} {vs vs′ : W ⊩⋆ Γ} {a a′ : W ⊩ A} →
              (es : Eq⋆ vs vs′) (e : Eq a a′) →
              Eq⋆ [ vs , a ] [ vs′ , a′ ]

  data Un⋆ : ∀ {Γ W} → W ⊩⋆ Γ → Set where
    []    : ∀ {W} →
              Un⋆ ([] {W})
    [_,_] : ∀ {Γ A W} {vs : W ⊩⋆ Γ} {a : W ⊩ A} →
              (us : Un⋆ vs) (u : Un a) →
              Un⋆ [ vs , a ]

  reflEq⋆ : ∀ {Γ W} {vs : W ⊩⋆ Γ} → Un⋆ vs → Eq⋆ vs vs
  reflEq⋆ []         = []
  reflEq⋆ [ us , u ] = [ reflEq⋆ us , reflEq u ]

  symEq⋆ : ∀ {Γ W} {vs vs′ : W ⊩⋆ Γ} → Eq⋆ vs vs′ → Eq⋆ vs′ vs
  symEq⋆ []         = []
  symEq⋆ [ es , e ] = [ symEq⋆ es , symEq e ]

  transEq⋆ : ∀ {Γ W} {vs vs′ vs″ : W ⊩⋆ Γ} → Eq⋆ vs vs′ → Eq⋆ vs′ vs″ → Eq⋆ vs vs″
  transEq⋆ []         []           = []
  transEq⋆ [ es , e ] [ es′ , e′ ] = [ transEq⋆ es es′ , transEq e e′ ]

  ≡→Eq⋆ : ∀ {Γ W} {vs vs′ : W ⊩⋆ Γ} → vs ≡ vs′ → Un⋆ vs → Eq⋆ vs vs′
  ≡→Eq⋆ refl us = reflEq⋆ us

  module Eq⋆-Reasoning where
    infix 1 begin_
    begin_ : ∀ {Γ W} {vs vs′ : W ⊩⋆ Γ} → Eq⋆ vs vs′ → Eq⋆ vs vs′
    begin es = es

    infixr 2 _Eq⋆⟨⟩_
    _Eq⋆⟨⟩_ : ∀ {Γ W} (vs {vs′} : W ⊩⋆ Γ) → Eq⋆ vs vs′ → Eq⋆ vs vs′
    vs Eq⋆⟨⟩ es = es

    infixr 2 _Eq⋆⟨_⟩_
    _Eq⋆⟨_⟩_ : ∀ {Γ W} (vs {vs′ vs″} : W ⊩⋆ Γ) → Eq⋆ vs vs′ → Eq⋆ vs′ vs″ → Eq⋆ vs vs″
    vs Eq⋆⟨ es ⟩ es′ = transEq⋆ es es′

    infixr 2 _≡⟨⟩_
    _≡⟨⟩_ : ∀ {Γ W} (vs {vs′} : W ⊩⋆ Γ) → Eq⋆ vs vs′ → Eq⋆ vs vs′
    vs ≡⟨⟩ es = es

    infixr 2 _≡⟨_∣_⟩_
    _≡⟨_∣_⟩_ : ∀ {Γ W} (vs {vs′ vs″} : W ⊩⋆ Γ) → vs ≡ vs′ → Un⋆ vs → Eq⋆ vs′ vs″ → Eq⋆ vs vs″
    vs ≡⟨ es ∣ us ⟩ es′ = transEq⋆ (≡→Eq⋆ es us) es′

    infix 3 _∎⟨_⟩
    _∎⟨_⟩ : ∀ {Γ W} (vs : W ⊩⋆ Γ) → Un⋆ vs → Eq⋆ vs vs
    vs ∎⟨ us ⟩ = reflEq⋆ us


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

module _ {{𝔪 : 𝔐}} where
  open 𝔐 𝔪

  -- conglookupEq
  postulate
    getEq : ∀ {Γ A W} {vs vs′ : W ⊩⋆ Γ} →
              (i : Γ ∋ A) → Eq⋆ vs vs′ →
              Eq (get vs i) (get vs′ i)

  -- cong↑⟨_⟩Eq⋆
  postulate
    accEq⋆ : ∀ {Γ V W} {vs vs′ : W ⊩⋆ Γ} →
               (xs : V ⊒ W) → Eq⋆ vs vs′ →
               Eq⋆ (acc⋆ xs vs) (acc⋆ xs vs′)

  -- cong↓⟨_⟩Eq⋆
  postulate
    getEq⋆ : ∀ {Γ Δ W} {vs vs′ : W ⊩⋆ Δ} →
               (xs : Δ ∋⋆ Γ) → Eq⋆ vs vs′ →
               Eq⋆ (get⋆ vs xs) (get⋆ vs′ xs)

  -- conglookup𝒰
  postulate
    getUn : ∀ {Γ A W} {vs : W ⊩⋆ Γ} →
              (i : Γ ∋ A) → Un⋆ vs →
              Un (get vs i)

  -- cong↑⟨_⟩𝒰⋆
  postulate
    accUn⋆ : ∀ {Γ V W} {vs : W ⊩⋆ Γ} →
               (xs : V ⊒ W) → Un⋆ vs →
               Un⋆ (acc⋆ xs vs)

  -- cong↓⟨_⟩𝒰⋆
  postulate
    getUn⋆ : ∀ {Γ Δ W} {vs : W ⊩⋆ Δ} →
               (xs : Δ ∋⋆ Γ) → Un⋆ vs →
               Un⋆ (get⋆ vs xs)


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

module _ {{𝔪 : 𝔐}} where
  open 𝔐 𝔪

  -- aux₄₂₁
  postulate
    getgetEq : ∀ {Γ Δ A W} {vs : W ⊩⋆ Δ} →
                 (xs : Δ ∋⋆ Γ) (i : Δ ∋ A) (j : Γ ∋ A) → Un⋆ vs →
                 Eq (get vs i) (get (get⋆ vs xs) j)

  -- conglookup↑⟨_⟩Eq
  postulate
    accgetEq : ∀ {Γ A V W} {vs : W ⊩⋆ Γ} →
                 (xs : V ⊒ W) (i : Γ ∋ A) → Un⋆ vs →
                 Eq (acc xs (get vs i)) (get (acc⋆ xs vs) i)

  -- aux₄₂₃
  postulate
    zapgetEq⋆ : ∀ {Γ Δ A W} {vs : W ⊩⋆ Δ} {a : W ⊩ A} →
                  (xs : [ Δ , A ] ∋⋆ Γ) (ys : Δ ∋⋆ Γ) → Un⋆ vs →
                  Eq⋆ (get⋆ [ vs , a ] xs) (get⋆ vs ys)

  -- aux₄₂₄
  postulate
    idgetEq⋆ : ∀ {Γ W} {vs : W ⊩⋆ Γ} →
                 Un⋆ vs →
                 Eq⋆ (get⋆ vs idᵣ) vs

  -- aux₄₂₅
  postulate
    idaccEq⋆ : ∀ {Γ W} {vs : W ⊩⋆ Γ} →
                 Un⋆ vs →
                 Eq⋆ (acc⋆ id⊒ vs) vs

  -- aux₄₂₆
  postulate
    getgetEq⋆ : ∀ {Γ Δ Φ W} {vs : W ⊩⋆ Φ} →
                  (xs : Φ ∋⋆ Δ) (ys : Δ ∋⋆ Γ) → Un⋆ vs →
                  Eq⋆ (get⋆ (get⋆ vs xs) ys) (get⋆ vs (xs ○ ys))

  -- aux₄₂₇
  postulate
    accaccEq⋆ : ∀ {Γ U V W} {vs : W ⊩⋆ Γ} →
                  (xs : U ⊒ V) (ys : V ⊒ W) → Un⋆ vs →
                  Eq⋆ (acc⋆ xs (acc⋆ ys vs)) (acc⋆ (xs ◇ ys) vs)

  -- aux₄₂₈
  postulate
    accgetEq⋆ : ∀ {Γ Δ V W} {vs : W ⊩⋆ Δ} →
                  (xs : Δ ∋⋆ Γ) (ys : V ⊒ W) → Un⋆ vs →
                  Eq⋆ (acc⋆ ys (get⋆ vs xs)) (get⋆ (acc⋆ ys vs) xs)


--------------------------------------------------------------------------------
--
-- Evaluation

module _ {{𝔪 : 𝔐}} where
  open 𝔐 𝔪

  ⟦_⟧ : ∀ {Γ A W} → Γ ⊢ A → W ⊩⋆ Γ → W ⊩ A
  ⟦ ν i ⟧   vs = get vs i
  ⟦ ƛ M ⟧   vs = ⟦ƛ⟧ (λ xs a → ⟦ M ⟧ [ acc⋆ xs vs , a ])
  ⟦ M ∙ N ⟧ vs = ⟦ M ⟧ vs ◎⟨ id⊒ ⟩ ⟦ N ⟧ vs

  ⟦_⟧⋆ : ∀ {Γ Δ W} → Δ ⊢⋆ Γ → W ⊩⋆ Δ → W ⊩⋆ Γ
  ⟦ [] ⟧⋆         vs = []
  ⟦ [ xs , x ] ⟧⋆ vs = [ ⟦ xs ⟧⋆ vs , ⟦ x ⟧ vs ]


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

instance
  canon : 𝔐
  canon = record
    { 𝒲      = 𝒞
    ; 𝒢      = _⊢ •
    ; _⊒_    = _∋⋆_
    ; id⊒    = idᵣ
    ; _◇_    = _○_
    ; lid◇   = id₁○
    ; rid◇   = id₂○
    ; assoc◇ = assoc○
    }


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

mutual
  reify : ∀ {A Γ} → Γ ⊩ A → Γ ⊢ A
  reify {•}     f = ⟦g⟧⟨ idᵣ ⟩ f
  reify {A ⊃ B} f = ƛ (reify (f ◎⟨ wkᵣ idᵣ ⟩ ⟪ν⟫ zero))

  ⟪_⟫ : ∀ {A Γ} → (∀ {Δ} → Δ ∋⋆ Γ → Δ ⊢ A) → Γ ⊩ A
  ⟪_⟫ {•}     f = ⟦G⟧ (λ xs   → f xs)
  ⟪_⟫ {A ⊃ B} f = ⟦ƛ⟧ (λ xs a → ⟪ (λ ys → f (ys ○ xs) ∙ reify (acc ys a)) ⟫)

  ⟪ν⟫ : ∀ {Γ A} → Γ ∋ A → Γ ⊩ A
  ⟪ν⟫ i = ⟪ (λ xs → ren xs (ν i)) ⟫

postulate
  aux₄₄₁ : ∀ {A Γ} →
             (f f′ : ∀ {Δ} → Δ ∋⋆ Γ → Δ ⊢ A) →
             (∀ {Δ} → (xs : Δ ∋⋆ Γ) → f xs ≡ f′ xs) →
             Eq (⟪ f ⟫) (⟪ f′ ⟫)

postulate
  aux₄₄₂ : ∀ {A Γ Δ} →
             (xs : Δ ∋⋆ Γ) (f : (∀ {Δ} → Δ ∋⋆ Γ → Δ ⊢ A)) →
             Eq (acc xs ⟪ f ⟫) (⟪ (λ ys → f (ys ○ xs)) ⟫)


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

-- Theorem 1.
mutual
  postulate
    thm₁ : ∀ {Γ A} {a a′ : Γ ⊩ A} →
             Eq a a′ →
             reify a ≡ reify a′

  postulate
    ⟪ν⟫Un : ∀ {Γ A} → (i : Γ ∋ A) → Un (⟪ν⟫ i)

  postulate
    aux₄₄₃ : ∀ {A Γ} →
               (f : ∀ {Δ} → Δ ∋⋆ Γ → Δ ⊢ A) →
               Un (⟪ f ⟫)


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

⌊_⌋⊩⋆ : ∀ {Γ Δ} → Δ ∋⋆ Γ → Δ ⊩⋆ Γ
⌊ [] ⌋⊩⋆         = []
⌊ [ xs , x ] ⌋⊩⋆ = [ ⌊ xs ⌋⊩⋆ , ⟪ν⟫ x ]

id⊩⋆ : ∀ {Γ} → Γ ⊩⋆ Γ
id⊩⋆ = ⌊ idᵣ ⌋⊩⋆

nf : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A
nf M = reify (⟦ M ⟧ id⊩⋆)

-- Corollary 1.
postulate
  cor₁ : ∀ {Γ A} →
           (M M′ : Γ ⊢ A) → Eq (⟦ M ⟧ id⊩⋆) (⟦ M′ ⟧ id⊩⋆) →
           nf M ≡ nf M′


--------------------------------------------------------------------------------
--
-- Computability

data CV : ∀ {Γ A} → Γ ⊢ A → Γ ⊩ A → Set where
  cv• : ∀ {Γ} {M : Γ ⊢ •} {f : Γ ⊩ •} →
          (h : ∀ {Δ} →
                 (xs : Δ ∋⋆ Γ) →
                 sub ⌊ xs ⌋ M ≅ ⟦g⟧⟨ xs ⟩ f) →
          CV M f
  cv⊃ : ∀ {Γ A B} {M : Γ ⊢ A ⊃ B} {f : Γ ⊩ A ⊃ B} →
          (h : ∀ {Δ N a} →
                 (xs : Δ ∋⋆ Γ) → CV N a →
                 CV (sub ⌊ xs ⌋ M ∙ N) (f ◎⟨ xs ⟩ a)) →
          CV M f

data CV⋆ : ∀ {Γ Δ} → Δ ⊢⋆ Γ → Δ ⊩⋆ Γ → Set where
  []    : ∀ {Γ} {xs : Γ ⊢⋆ []} →
            CV⋆ xs []
  [_,_] : ∀ {Γ Δ A} {xs : Δ ⊢⋆ [ Γ , A ]} {vs : Δ ⊩⋆ Γ} {a : Δ ⊩ A} →
            (cs : CV⋆ (xs ● ⌊ wkᵣ {A} idᵣ ⌋) vs) (c : CV (sub xs (ν zero)) a) →
            CV⋆ xs [ vs , a ]


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

postulate
  congCV : ∀ {Γ A} {M M′ : Γ ⊢ A} {a : Γ ⊩ A} →
             M ≅ M′ → CV M′ a →
             CV M a

-- cong↑⟨_⟩CV
postulate
  accCV : ∀ {Γ Δ A} {M : Γ ⊢ A} {a : Γ ⊩ A} →
            (xs : Δ ∋⋆ Γ) → CV M a →
            CV (sub ⌊ xs ⌋ M) (acc xs a)

-- flip conglookupCV
postulate
  getCV : ∀ {Γ Δ A} {xs : Δ ⊢⋆ Γ} {vs : Δ ⊩⋆ Γ} →
            (i : Γ ∋ A) → CV⋆ xs vs →
            CV (sub xs (ν i)) (get vs i)

-- cong↑⟨_⟩CV⋆
postulate
  accCV⋆ : ∀ {Γ Δ Φ} {xs : Δ ⊢⋆ Γ} {vs : Δ ⊩⋆ Γ} →
             (ys : Φ ∋⋆ Δ) → CV⋆ xs vs →
             CV⋆ (⌊ ys ⌋ ● xs) (acc⋆ ys vs)

-- cong↓⟨_⟩CV⋆
postulate
  getCV⋆ : ∀ {Γ Δ Φ} {xs : Δ ⊢⋆ Γ} {vs : Δ ⊩⋆ Γ} →
             (ys : Γ ∋⋆ Φ) → CV⋆ xs vs →
             CV⋆ (xs ● ⌊ ys ⌋) (get⋆ vs ys)


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

-- Lemma 8.
postulate
  ⟦_⟧CV : ∀ {Γ Δ A} {xs : Δ ⊢⋆ Γ} {vs : Δ ⊩⋆ Γ} →
            (M : Γ ⊢ A) → CV⋆ xs vs →
            CV (sub xs M) (⟦ M ⟧ vs)

postulate
  ⟦_⟧CV⋆ : ∀ {Γ Δ Φ} {xs : Φ ⊢⋆ Δ} {vs : Φ ⊩⋆ Δ} →
             (ys : Δ ⊢⋆ Γ) → CV⋆ xs vs →
             CV⋆ (xs ● ys) (⟦ ys ⟧⋆ vs)


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

-- Lemma 9.
mutual
  postulate
    lem₉ : ∀ {Γ A} {M : Γ ⊢ A} {a : Γ ⊩ A} →
             CV M a →
             M ≅ reify a

  postulate
    aux₄₆₈ : ∀ {A Γ} {M : Γ ⊢ A} {f : ∀ {Δ} → Δ ∋⋆ Γ → Δ ⊢ A} →
               (∀ {Δ} → (xs : Δ ∋⋆ Γ) → sub ⌊ xs ⌋ M ≅ f xs) →
               CV M (⟪ f ⟫)

postulate
  ⌊_⌋CV⋆ : ∀ {Γ Δ} → (xs : Δ ∋⋆ Γ) → CV⋆ ⌊ xs ⌋ ⌊ xs ⌋⊩⋆

idCV⋆ : ∀ {Γ} → CV⋆ ⌊ idᵣ ⌋ (id⊩⋆ {Γ})
idCV⋆ = ⌊ idᵣ ⌋CV⋆

postulate
  aux₄₆₉ : ∀ {Γ A} →
             (M : Γ ⊢ A) →
             sub ⌊ idᵣ ⌋ M ≅ nf M


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

-- Theorem 2.
postulate
  thm₂ : ∀ {Γ A} →
           (M : Γ ⊢ A) →
           M ≅ nf M

-- Theorem 3.
thm₃ : ∀ {Γ A} →
         (M M′ : Γ ⊢ A) → Eq (⟦ M ⟧ id⊩⋆) (⟦ M′ ⟧ id⊩⋆) →
         M ≅ M′
thm₃ M M′ e =
  begin
    M
  ≅⟨ thm₂ M ⟩
    nf M
  ≡⟨ cor₁ M M′ e ⟩
    nf M′
  ≅⟨ sym≅ (thm₂ M′) ⟩
    M′
  ∎
  where open ≅-Reasoning


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

reify⋆ : ∀ {Γ Δ} → Δ ⊩⋆ Γ → Δ ⊢⋆ Γ
reify⋆ []         = []
reify⋆ [ vs , v ] = [ reify⋆ vs , reify v ]

nf⋆ : ∀ {Γ Δ} → Δ ⊢⋆ Γ → Δ ⊢⋆ Γ
nf⋆ xs = reify⋆ (⟦ xs ⟧⋆ id⊩⋆)

thm₁ₛ : ∀ {Γ Δ} {vs vs′ : Δ ⊩⋆ Γ} →
          Eq⋆ vs vs′ →
          reify⋆ vs ≡ reify⋆ vs′
thm₁ₛ []         = refl
thm₁ₛ [ es , e ] = cong² [_,_] (thm₁ₛ es) (thm₁ e)

cor₁ₛ : ∀ {Γ Δ} →
          (xs xs′ : Δ ⊢⋆ Γ) → Eq⋆ (⟦ xs ⟧⋆ id⊩⋆) (⟦ xs′ ⟧⋆ id⊩⋆) →
          nf⋆ xs ≡ nf⋆ xs′
cor₁ₛ xs xs′ = thm₁ₛ

-- TODO: Do we need _≅⋆_?

-- lem₉ₛ : ∀ {Γ Δ} {xs : Δ ⊢⋆ Γ} {vs : Δ ⊩⋆ Γ} →
--           CV⋆ xs vs →
--           xs ≅⋆ reify⋆ vs
-- lem₉ₛ []         = {!!}
-- lem₉ₛ [ cs , c ] = {!!}

-- aux₄₆₉ₛ⟨_⟩ : ∀ {Γ Δ} →
--                (c : Δ ⊇ Δ) (γ : Δ ⋙ Γ) →
--                γ ● π⟨ c ⟩ ≅ₛ nf⋆ γ

-- thm₂ₛ : ∀ {Γ Δ} → (γ : Δ ⋙ Γ) →
--           γ ≅ₛ nf⋆ γ

-- thm₃ₛ : ∀ {Γ Δ} → (γ γ′ : Δ ⋙ Γ) → Eq⋆ (⟦ γ ⟧ₛ refl⊩⋆) (⟦ γ′ ⟧ₛ refl⊩⋆) →
--           γ ≅ₛ γ′


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

-- Un⟦_⟧
postulate
  ⟦_⟧Un : ∀ {Γ Δ A} {vs : Δ ⊩⋆ Γ} →
            (M : Γ ⊢ A) → Un⋆ vs →
            Un (⟦ M ⟧ vs)

-- 𝒰⋆⟦_⟧ₛ
postulate
  ⟦_⟧Un⋆ : ∀ {Γ Δ Φ} {vs : Φ ⊩⋆ Δ} →
                 (xs : Δ ⊢⋆ Γ) → Un⋆ vs →
                 Un⋆ (⟦ xs ⟧⋆ vs)

postulate
  ⟦_⟧Eq : ∀ {Γ Δ A} {vs vs′ : Δ ⊩⋆ Γ} →
                (M : Γ ⊢ A) → Eq⋆ vs vs′ → Un⋆ vs → Un⋆ vs′ →
                Eq (⟦ M ⟧ vs) (⟦ M ⟧ vs′)

-- Eq⋆⟦_⟧ₛ
postulate
  ⟦_⟧Eq⋆ : ∀ {Γ Δ Φ} {vs vs′ : Φ ⊩⋆ Δ} →
                 (xs : Δ ⊢⋆ Γ) → Eq⋆ vs vs′ → Un⋆ vs → Un⋆ vs′ →
                 Eq⋆ (⟦ xs ⟧⋆ vs) (⟦ xs ⟧⋆ vs′)

-- ↑⟨_⟩Eq⟦_⟧
postulate
  acc⟦_⟧Eq : ∀ {Γ Δ Φ A} {vs : Δ ⊩⋆ Γ} →
               (M : Γ ⊢ A) (xs : Φ ∋⋆ Δ) → Un⋆ vs →
               Eq (acc xs (⟦ M ⟧ vs)) (⟦ M ⟧ (acc⋆ xs vs))

-- ↑⟨_⟩Eq⋆⟦_⟧ₛ
postulate
  acc⟦_⟧Eq⋆ : ∀ {Γ Δ Φ Ψ} {vs : Φ ⊩⋆ Δ} →
                (xs : Δ ⊢⋆ Γ) (ys : Ψ ∋⋆ Φ) → Un⋆ vs →
                Eq⋆ (acc⋆ ys (⟦ xs ⟧⋆ vs)) (⟦ xs ⟧⋆ (acc⋆ ys vs))


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

postulate
  aux₄₈₁ : ∀ {Γ Δ A} {vs : Δ ⊩⋆ Γ} {a : Δ ⊩ A} →
             Un⋆ vs →
             Eq⋆ (get⋆ [ vs , a ] (wkᵣ idᵣ)) vs


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

module _ where
  open Eq-Reasoning

  oops₄ : ∀ {Γ Δ A B V W} {vs : W ⊩⋆ Δ} {a : V ⊩ A} →
            (xs : Δ ∋⋆ Γ) (ys : V ∋⋆ W) (M : [ Γ , A ] ⊢ B) → Un⋆ vs → Un a →
            Eq (⟦ ren (liftᵣ xs) M ⟧ [ acc⋆ ys vs , a ]) (⟦ M ⟧ [ acc⋆ ys (get⋆ vs xs) , a ])
  oops₄ {vs = vs} {a} xs ys (ν zero)    us u = reflEq u
  oops₄ {vs = vs} {a} xs ys (ν (suc i)) us u =
    begin
      ⟦ ren (liftᵣ xs) (ν (suc i)) ⟧ [ acc⋆ ys vs , a ]
    ≡⟨⟩
      get [ acc⋆ ys vs , a ] (getᵣ (wkᵣ xs) i)
    ≡⟨ cong² get refl (wkgetᵣ xs i) ∣ getUn (getᵣ (wkᵣ xs) i) [ accUn⋆ ys us , u ] ⟩
      get [ acc⋆ ys vs , a ] (suc (getᵣ xs i))
    ≡⟨⟩
      get (acc⋆ ys vs) (getᵣ xs i)
    Eq⟨ getgetEq xs (getᵣ xs i) i (accUn⋆ ys us) ⟩
      get (get⋆ (acc⋆ ys vs) xs) i
    Eq⟨ getEq i (symEq⋆ (accgetEq⋆ xs ys us)) ⟩
      get (acc⋆ ys (get⋆ vs xs)) i
    ≡⟨⟩
      ⟦ ν (suc i) ⟧ [ acc⋆ ys (get⋆ vs xs) , a ]
    ∎⟨ ⟦ ν (suc i) ⟧Un [ accUn⋆ ys (getUn⋆ xs us) , u ] ⟩
  oops₄ {vs = vs} {a} xs ys (ƛ M) us u =
    begin
      ⟦ ren (liftᵣ xs) (ƛ M) ⟧ [ acc⋆ ys vs , a ]
    ≡⟨⟩
      ⟦ƛ⟧ (λ zs a′ → ⟦ ren (liftᵣ (liftᵣ xs)) M ⟧ [ [ acc⋆ zs (acc⋆ ys vs) , acc zs a ] , a′ ] )
    Eq⟨ eq⊃ (λ zs u′ → oops₄ (liftᵣ xs) zs M [ accUn⋆ ys us , u ] u′) ⟩ -- ‼
      ⟦ƛ⟧ (λ zs a′ → ⟦ M ⟧ [ acc⋆ zs (get⋆ [ acc⋆ ys vs , a ] (liftᵣ xs)) , a′ ] )
    Eq⟨ eq⊃ (λ zs u′ → ⟦ M ⟧Eq [ [ accEq⋆ zs (symEq⋆ (transEq⋆ (accgetEq⋆ xs ys us)
                                                                (symEq⋆ (zapgetEq⋆ (wkᵣ xs) xs (accUn⋆ ys us))))) , reflEq (accUn zs u) ] , reflEq u′ ]
                                [ [ accUn⋆ zs (getUn⋆ (wkᵣ xs) [ accUn⋆ ys us , u ]) , accUn zs u ] , u′ ]
                                [ [ accUn⋆ zs (accUn⋆ ys (getUn⋆ xs us)) , accUn zs u ] , u′ ]) ⟩
      ⟦ƛ⟧ (λ zs a′ → ⟦ M ⟧ [ [ acc⋆ zs (acc⋆ ys (get⋆ vs xs)) , acc zs a ] , a′ ])
    ≡⟨⟩
      ⟦ ƛ M ⟧ [ acc⋆ ys (get⋆ vs xs) , a ]
    ∎⟨ ⟦ ƛ M ⟧Un [ accUn⋆ ys (getUn⋆ xs us) , u ] ⟩
  oops₄ {vs = vs} {a} xs ys (M ∙ N) us u =
    begin
      ⟦ ren (liftᵣ xs) (M ∙ N) ⟧ [ acc⋆ ys vs , a ]
    ≡⟨⟩
      ⟦ ren (liftᵣ xs) M ⟧ [ acc⋆ ys vs , a ] ◎⟨ idᵣ ⟩ ⟦ ren (liftᵣ xs) N ⟧ [ acc⋆ ys vs , a ]
    Eq⟨ ◎Eq idᵣ (oops₄ xs ys M us u) (⟦ ren (liftᵣ xs) M ⟧Un [ accUn⋆ ys us , u ]) (⟦ M ⟧Un [ accUn⋆ ys (getUn⋆ xs us) , u ]) -- ‼
                (oops₄ xs ys N us u) (⟦ ren (liftᵣ xs) N ⟧Un [ accUn⋆ ys us , u ]) (⟦ N ⟧Un [ accUn⋆ ys (getUn⋆ xs us) , u ]) ⟩ -- ‼
      ⟦ M ⟧ [ acc⋆ ys (get⋆ vs xs) , a ] ◎⟨ idᵣ ⟩ ⟦ N ⟧ [ acc⋆ ys (get⋆ vs xs) , a ]
    ≡⟨⟩
      ⟦ M ∙ N ⟧ [ acc⋆ ys (get⋆ vs xs) , a ]
    ∎⟨ ⟦ M ∙ N ⟧Un [ accUn⋆ ys (getUn⋆ xs us) , u ] ⟩

  oops₃ : ∀ {Γ Δ A C W} {vs : W ⊩⋆ Δ} {a : W ⊩ A} →
            (xs : Δ ∋⋆ Γ) (M : Γ ⊢ C) → Un⋆ vs → Un a →
            Eq (⟦ ren (wkᵣ xs) M ⟧ [ vs , a ]) (⟦ M ⟧ (get⋆ vs xs))
  oops₃ {vs = vs} {a} xs (ν i) us u =
    begin
      ⟦ ren (wkᵣ xs) (ν i) ⟧ [ vs , a ]
    ≡⟨⟩
      get [ vs , a ] (getᵣ (wkᵣ xs) i)
    Eq⟨ getgetEq (wkᵣ xs) (getᵣ (wkᵣ xs) i) i [ us , u ] ⟩
      get (get⋆ [ vs , a ] (wkᵣ xs)) i
    Eq⟨ getEq i (zapgetEq⋆ (wkᵣ xs) xs us) ⟩
      get (get⋆ vs xs) i
    ≡⟨⟩
      ⟦ ν i ⟧ (get⋆ vs xs)
    ∎⟨ ⟦ ν i ⟧Un (getUn⋆ xs us) ⟩
  oops₃ {vs = vs} {a} xs (ƛ M) us u =
    begin
      ⟦ ren (wkᵣ xs) (ƛ M) ⟧ [ vs , a ]
    ≡⟨⟩
      ⟦ƛ⟧ (λ ys a′ → ⟦ ren (liftᵣ (wkᵣ xs)) M ⟧ [ [ acc⋆ ys vs , acc ys a ] , a′ ])
    Eq⟨ eq⊃ (λ ys u′ → oops₄ (wkᵣ xs) ys M [ us , u ] u′) ⟩ -- ‼
      ⟦ƛ⟧ (λ ys a′ → ⟦ M ⟧ [ acc⋆ ys (get⋆ [ vs , a ] (wkᵣ xs)) , a′ ])
    Eq⟨ eq⊃ (λ ys u′ → ⟦ M ⟧Eq [ accEq⋆ ys (zapgetEq⋆ (wkᵣ xs) xs us) , reflEq u′ ]
                                [ accUn⋆ ys (getUn⋆ (wkᵣ xs) [ us , u ]) , u′ ]
                                [ accUn⋆ ys (getUn⋆ xs us) , u′ ]) ⟩
      ⟦ƛ⟧ (λ ys a′ → ⟦ M ⟧ [ acc⋆ ys (get⋆ vs xs) , a′ ])
    ≡⟨⟩
      ⟦ ƛ M ⟧ (get⋆ vs xs)
    ∎⟨ ⟦ ƛ M ⟧Un (getUn⋆ xs us) ⟩
  oops₃ {vs = vs} {a} xs (M ∙ N) us u =
    begin
      ⟦ ren (wkᵣ xs) (M ∙ N) ⟧ [ vs , a ]
    ≡⟨⟩
      (⟦ ren (wkᵣ xs) M ⟧ [ vs , a ] ◎⟨ idᵣ ⟩ ⟦ ren (wkᵣ xs) N ⟧ [ vs , a ])
    Eq⟨ ◎Eq idᵣ (oops₃ xs M us u) (⟦ ren (wkᵣ xs) M ⟧Un [ us , u ]) (⟦ M ⟧Un (getUn⋆ xs us)) -- ‼
                (oops₃ xs N us u) (⟦ ren (wkᵣ xs) N ⟧Un [ us , u ]) (⟦ N ⟧Un (getUn⋆ xs us)) ⟩ -- ‼
      (⟦ M ⟧ (get⋆ vs xs) ◎⟨ idᵣ ⟩ ⟦ N ⟧ (get⋆ vs xs))
    ≡⟨⟩
      ⟦ M ∙ N ⟧ (get⋆ vs xs)
    ∎⟨ ⟦ M ∙ N ⟧Un (getUn⋆ xs us) ⟩

  oops₂ : ∀ {Γ A C W} {vs : W ⊩⋆ Γ} {a : W ⊩ A} →
            (M : Γ ⊢ C) → Un⋆ vs → Un a →
            Eq (⟦ wk M ⟧ [ vs , a ]) (⟦ M ⟧ vs)
  oops₂ {vs = vs} {a} M us u =
    begin
      ⟦ wk M ⟧ [ vs , a ]
    Eq⟨ oops₃ idᵣ M us u ⟩ -- ‼
      ⟦ M ⟧ (get⋆ vs idᵣ)
    Eq⟨ ⟦ M ⟧Eq (idgetEq⋆ us) (getUn⋆ idᵣ us) us ⟩
      ⟦ M ⟧ vs
    ∎⟨ ⟦ M ⟧Un us ⟩


  ⟦sub⟧ : ∀ {Γ Δ A} → Δ ⊩⋆ Γ → Γ ⊩ A → Δ ⊩ A
  ⟦sub⟧ vs a = ⟦ sub (reify⋆ vs) (reify a) ⟧ id⊩⋆

  ⟦sub⋆⟧ : ∀ {Γ Δ Φ} → Φ ⊩⋆ Δ → Δ ⊩⋆ Γ → Φ ⊩⋆ Γ
  ⟦sub⋆⟧ vs []         = []
  ⟦sub⋆⟧ vs [ ws , w ] = [ ⟦sub⋆⟧ vs ws , ⟦sub⟧ vs w ]


  genoops₁ : ∀ {Γ Δ A C W} {vs : W ⊩⋆ Δ} {a : W ⊩ A} →
               (xs : Δ ⊢⋆ Γ) (M : Γ ⊢ C) → Un⋆ vs → Un a →
               Eq (⟦ sub (liftₛ xs) (wk M) ⟧ [ vs , a ]) (⟦ sub xs M ⟧ vs)
  genoops₁ {vs = vs} {a} xs (ν i) us u =
    begin
      ⟦ sub (liftₛ xs) (wk (ν i)) ⟧ [ vs , a ]
    ≡⟨⟩
      ⟦ getₛ (liftₛ xs) (getᵣ (wkᵣ idᵣ) i) ⟧ [ vs , a ]
    ≡⟨ cong² ⟦_⟧ (cong² getₛ refl (wkgetᵣ idᵣ i)) refl ∣ ⟦ getₛ (liftₛ xs) (getᵣ (wkᵣ idᵣ) i) ⟧Un [ us , u ] ⟩
      ⟦ getₛ (liftₛ xs) (suc (getᵣ idᵣ i)) ⟧ [ vs , a ]
    ≡⟨ cong² ⟦_⟧ (cong² getₛ refl (idgetᵣ i)) refl ∣ ⟦ getₛ (wkₛ xs) (getᵣ idᵣ i) ⟧Un [ us , u ] ⟩
      ⟦ getₛ (liftₛ xs) (suc i) ⟧ [ vs , a ]
    ≡⟨⟩
      ⟦ getₛ (wkₛ xs) i ⟧ [ vs , a ]
    ≡⟨ cong² ⟦_⟧ (wkgetₛ xs i) refl ∣ ⟦ getₛ (wkₛ xs) i ⟧Un [ us , u ] ⟩
      ⟦ wk (getₛ xs i) ⟧ [ vs , a ]
    Eq⟨ oops₂ (getₛ xs i) us u ⟩ -- ‼
      ⟦ getₛ xs i ⟧ vs
    ≡⟨⟩
      ⟦ sub xs (ν i) ⟧ vs
    ∎⟨ ⟦ getₛ xs i ⟧Un us ⟩
  genoops₁ {vs = vs} {a} xs (ƛ M) us u =
    begin
      ⟦ sub (liftₛ xs) (wk (ƛ M)) ⟧ [ vs , a ]
    ≡⟨⟩
      ⟦ƛ⟧ (λ ys a′ → ⟦ sub (liftₛ (liftₛ xs)) (ren (liftᵣ (wkᵣ idᵣ)) M) ⟧ [ [ acc⋆ ys vs , acc ys a ] , a′ ])
    Eq⟨ {!!} ⟩
      ⟦ƛ⟧ (λ ys a′ → ⟦ sub xs {!!} ⟧ (acc⋆ ys vs))
    Eq⟨ eq⊃ (λ ys u′ → symEq (genoops₁ xs {!!} (accUn⋆ ys us) u′) ) ⟩
      ⟦ƛ⟧ (λ ys a′ → ⟦ sub (liftₛ xs) M ⟧ [ acc⋆ ys vs , a′ ])
    ≡⟨⟩
      ⟦ sub xs (ƛ M) ⟧ vs
    ∎⟨ ⟦ sub xs (ƛ M) ⟧Un us ⟩
  genoops₁ {vs = vs} {a} xs (M ∙ N) us u =
    begin
      ⟦ sub (liftₛ xs) (wk (M ∙ N)) ⟧ [ vs , a ]
    ≡⟨⟩
      (⟦ sub (liftₛ xs) (ren (wkᵣ idᵣ) M) ⟧ [ vs , a ] ◎⟨ idᵣ ⟩ ⟦ sub (liftₛ xs) (ren (wkᵣ idᵣ) N) ⟧ [ vs , a ])
    Eq⟨ ◎Eq idᵣ (genoops₁ xs M us u) (⟦ sub (liftₛ xs) (wk M) ⟧Un [ us , u ]) (⟦ sub xs M ⟧Un us)
                (genoops₁ xs N us u) (⟦ sub (liftₛ xs) (wk N) ⟧Un [ us , u ]) (⟦ sub xs N ⟧Un us) ⟩
      (⟦ sub xs M ⟧ vs ◎⟨ idᵣ ⟩ ⟦ sub xs N ⟧ vs)
    ≡⟨⟩
      ⟦ sub xs (M ∙ N) ⟧ vs
    ∎⟨ ⟦ sub xs (M ∙ N) ⟧Un us ⟩

  oops₁ : ∀ {Γ Δ A B W} {vs : W ⊩⋆ Δ} →
            (xs : Δ ⊢⋆ Γ) (M : [ Γ , A ] ⊢ B) (N : Δ ⊢ A) → Un⋆ vs →
            Eq (⟦ sub (liftₛ xs) M ⟧ [ vs , ⟦ N ⟧ vs ]) (⟦ sub [ xs , N ] M ⟧ vs)

  oops₁ {vs = vs} xs (ν zero)    N us = reflEq (⟦ N ⟧Un us)
  oops₁ {vs = vs} xs (ν (suc i)) N us =
    begin
      ⟦ sub (liftₛ xs) (ν (suc i)) ⟧ [ vs , ⟦ N ⟧ vs ]
    ≡⟨⟩
      ⟦ getₛ (wkₛ xs) i ⟧ [ vs , ⟦ N ⟧ vs ]
    ≡⟨ cong² ⟦_⟧ (wkgetₛ xs i) refl ∣ ⟦ getₛ (wkₛ xs) i ⟧Un [ us , ⟦ N ⟧Un us ] ⟩
      ⟦ wk (getₛ xs i) ⟧ [ vs , ⟦ N ⟧ vs ]
    Eq⟨ oops₂ (getₛ xs i) us (⟦ N ⟧Un us) ⟩ -- ‼
      ⟦ getₛ xs i ⟧ vs
    ≡⟨⟩
      ⟦ sub [ xs , N ] (ν (suc i)) ⟧ vs
    ∎⟨ ⟦ getₛ xs i ⟧Un us ⟩

  oops₁ {vs = vs} xs (ƛ M) N us =
    begin
      ⟦ sub (liftₛ xs) (ƛ M) ⟧ [ vs , ⟦ N ⟧ vs ]
    ≡⟨⟩
      ⟦ƛ⟧ (λ ys a → ⟦ sub (liftₛ (liftₛ xs)) M ⟧ [ [ acc⋆ ys vs , acc ys (⟦ N ⟧ vs) ] , a ])
    Eq⟨ eq⊃ (λ ys {a} u → {!!}) ⟩
      ⟦ƛ⟧ (λ ys a → ⟦ sub (liftₛ [ xs , N ]) M ⟧ [ acc⋆ ys vs , a ])
    ≡⟨⟩
      ⟦ sub [ xs , N ] (ƛ M) ⟧ vs
    ∎⟨ ⟦ sub [ xs , N ] (ƛ M) ⟧Un us ⟩

--  oops₁ {vs = vs} xs (ƛ M) N us =
--    begin
--      ⟦ sub (liftₛ xs) (ƛ M) ⟧ [ vs , ⟦ N ⟧ vs ]
--    ≡⟨⟩
--      ⟦ƛ⟧ (λ ys a → ⟦ sub (liftₛ (liftₛ xs)) M ⟧ [ [ acc⋆ ys vs , acc ys (⟦ N ⟧ vs) ] , a ])
--    ≡⟨⟩
--      ⟦ƛ⟧ (λ ys a → ⟦ sub (liftₛ [ wkₛ xs , ν zero ]) M ⟧ [ [ acc⋆ ys vs , acc ys (⟦ N ⟧ vs) ] , a ])
--    Eq⟨ eq⊃ (λ ys u → {!!}) ⟩
--      ⟦ƛ⟧ (λ ys a → ⟦ sub (liftₛ [ wkₛ xs , wk N   ]) M ⟧ [ [ acc⋆ ys vs , a                 ] , a ])
--    ≡⟨⟩
--      ⟦ƛ⟧ (λ ys a → ⟦ sub (liftₛ (wkₛ [ xs , N ])) M ⟧ [ [ acc⋆ ys vs , a ] , a ])
--    Eq⟨ eq⊃ (λ ys u → oops₁ (wkₛ [ xs , N ]) M (ν zero) [ accUn⋆ ys us , u ]) ⟩
--      ⟦ƛ⟧ (λ ys a → ⟦ sub [ wkₛ [ xs , N ] , ν zero ] M ⟧ [ acc⋆ ys vs , a ])
--    ≡⟨⟩
--      ⟦ƛ⟧ (λ ys a → ⟦ sub (liftₛ [ xs , N ]) M ⟧ [ acc⋆ ys vs , a ])
--    ≡⟨⟩
--      ⟦ sub [ xs , N ] (ƛ M) ⟧ vs
--    ∎⟨ ⟦ sub [ xs , N ] (ƛ M) ⟧Un us ⟩

  oops₁ {vs = vs} xs (M₁ ∙ M₂) N us =
    begin
      ⟦ sub (liftₛ xs) (M₁ ∙ M₂) ⟧ [ vs , ⟦ N ⟧ vs ]
    ≡⟨⟩
      (⟦ sub (liftₛ xs) M₁ ⟧ [ vs , ⟦ N ⟧ vs ] ◎⟨ idᵣ ⟩ ⟦ sub (liftₛ xs) M₂ ⟧ [ vs , ⟦ N ⟧ vs ])
    Eq⟨ ◎Eq idᵣ (oops₁ xs M₁ N us) (⟦ sub (liftₛ xs) M₁ ⟧Un [ us , ⟦ N ⟧Un us ]) (⟦ sub [ xs , N ] M₁ ⟧Un us) -- ‼
                (oops₁ xs M₂ N us) (⟦ sub (liftₛ xs) M₂ ⟧Un [ us , ⟦ N ⟧Un us ]) (⟦ sub [ xs , N ] M₂ ⟧Un us) ⟩ -- ‼
      (⟦ sub [ xs , N ] M₁ ⟧ vs ◎⟨ idᵣ ⟩ ⟦ sub [ xs , N ] M₂ ⟧ vs)
    ≡⟨⟩
      ⟦ sub [ xs , N ] (M₁ ∙ M₂) ⟧ vs
    ∎⟨ ⟦ sub [ xs , N ] (M₁ ∙ M₂) ⟧Un us ⟩


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

-- TODO: Generalise theorem 4 over models

mutual
  lemƛ : ∀ {Γ A B W} {vs : W ⊩⋆ Γ} {M M′ : [ Γ , A ] ⊢ B} →
           M ≅ M′ → Un⋆ vs →
           Eq (⟦ ƛ M ⟧ vs) (⟦ ƛ M′ ⟧ vs)
  lemƛ p us =
    eq⊃ (λ xs u →
      cong⟦ p ⟧Eq [ accUn⋆ xs us , u ])

  lem∙ : ∀ {Γ A B W} {vs : W ⊩⋆ Γ} {M M′ : Γ ⊢ A ⊃ B} {N N′ : Γ ⊢ A} →
           M ≅ M′ → N ≅ N′ → Un⋆ vs →
           Eq (⟦ M ∙ N ⟧ vs) (⟦ M′ ∙ N′ ⟧ vs)
  lem∙ {M = M} {M′} {N} {N′} p q us =
    ◎Eq idᵣ (cong⟦ p ⟧Eq us) (⟦ M ⟧Un us) (⟦ M′ ⟧Un us)
            (cong⟦ q ⟧Eq us) (⟦ N ⟧Un us) (⟦ N′ ⟧Un us)

  lemβ : ∀ {Γ Δ A B W} {vs : W ⊩⋆ Γ} →
           (xs : Γ ⊢⋆ Δ) (M : [ Δ , A ] ⊢ B) (N : Γ ⊢ A) → Un⋆ vs →
           Eq (⟦ sub xs (ƛ M) ∙ N ⟧ vs) (⟦ sub [ xs , N ] M ⟧ vs)
  lemβ {vs = vs} xs M N us =
    begin
      ⟦ sub (liftₛ xs) M ⟧ [ acc⋆ idᵣ vs , ⟦ N ⟧ vs ]
    Eq⟨ ⟦ sub (liftₛ xs) M ⟧Eq [ idaccEq⋆ us , reflEq (⟦ N ⟧Un us) ]
                               [ accUn⋆ idᵣ us , ⟦ N ⟧Un us ]
                               [ us , ⟦ N ⟧Un us ] ⟩
      ⟦ sub (liftₛ xs) M ⟧ [ vs , ⟦ N ⟧ vs ]
    Eq⟨ oops₁ xs M N us ⟩ -- ‼
      ⟦ sub [ xs , N ] M ⟧ vs
    ∎⟨ ⟦ sub [ xs , N ] M ⟧Un us ⟩
    where open Eq-Reasoning

  lemη : ∀ {Γ A B W} {vs : W ⊩⋆ Γ} →
           (M : Γ ⊢ A ⊃ B) → Un⋆ vs →
           Eq (⟦ M ⟧ vs) (⟦ ƛ (wk M ∙ ν zero) ⟧ vs)
  lemη {vs = vs} M us =
    eq⊃ (λ xs {a} u →
      begin
        ⟦ M ⟧ vs ◎⟨ xs ⟩ a
      Eq⟨ acc◎Eq xs (⟦ M ⟧Un us) u ⟩
        acc xs (⟦ M ⟧ vs) ◎⟨ idᵣ ⟩ a
      Eq⟨ ◎Eq idᵣ (acc⟦ M ⟧Eq xs us)
                  (accUn xs (⟦ M ⟧Un us))
                  (⟦ M ⟧Un (accUn⋆ xs us))
                  (reflEq u) u u ⟩
        ⟦ M ⟧ (acc⋆ xs vs) ◎⟨ idᵣ ⟩ a
      Eq⟨ ◎Eq idᵣ (symEq (oops₂ M (accUn⋆ xs us) u)) -- ‼
                  (⟦ M ⟧Un (accUn⋆ xs us))
                  (⟦ wk M ⟧Un [ accUn⋆ xs us , u ])
                  (reflEq u) u u ⟩
        ⟦ ren (wkᵣ idᵣ) M ⟧ [ acc⋆ xs vs , a ] ◎⟨ idᵣ ⟩ a
      ≡⟨⟩
        ⟦ wk M ⟧ [ acc⋆ xs vs , a ] ◎⟨ idᵣ ⟩ a
      ∎⟨ case ⟦ wk M ⟧Un [ accUn⋆ xs us , u ] of
           (λ { (un⊃ h₀ h₁ h₂) → h₀ idᵣ u }) ⟩)
      where open Eq-Reasoning

  -- Theorem 4.
  cong⟦_⟧Eq : ∀ {Γ A W} {M M′ : Γ ⊢ A} {vs : W ⊩⋆ Γ} →
                M ≅ M′ → Un⋆ vs →
                Eq (⟦ M ⟧ vs) (⟦ M′ ⟧ vs)
  cong⟦ refl≅ {M = M} ⟧Eq us = reflEq (⟦ M ⟧Un us)
  cong⟦ sym≅ p ⟧Eq        us = symEq (cong⟦ p ⟧Eq us)
  cong⟦ trans≅ p q ⟧Eq    us = transEq (cong⟦ p ⟧Eq us) (cong⟦ q ⟧Eq us)
  cong⟦ congƛ≅ p ⟧Eq      us = lemƛ p us
  cong⟦ cong∙≅ p q ⟧Eq    us = lem∙ p q us
  cong⟦ redβ≅ xs M N ⟧Eq  us = lemβ xs M N us
  cong⟦ expη≅ M ⟧Eq       us = lemη M us


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

-- Theorem 5.
thm₅ : ∀ {Γ A} → (M M′ : Γ ⊢ A) → nf M ≡ nf M′ → M ≅ M′
thm₅ M M′ p =
  begin
    M
  ≅⟨ thm₂ M ⟩
    nf M
  ≡⟨ p ⟩
    nf M′
  ≅⟨ sym≅ (thm₂ M′) ⟩
    M′
  ∎
  where open ≅-Reasoning


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

-- proj⟨_⟩𝒰⋆
⌊_⌋Un⋆ : ∀ {Γ Δ} → (xs : Δ ∋⋆ Γ) → Un⋆ ⌊ xs ⌋⊩⋆
⌊ [] ⌋Un⋆         = []
⌊ [ xs , x ] ⌋Un⋆ = [ ⌊ xs ⌋Un⋆ , ⟪ν⟫Un x ]

-- refl𝒰⋆
id⊩Un⋆ : ∀ {Γ} → Un⋆ (id⊩⋆ {Γ})
id⊩Un⋆ = ⌊ idᵣ ⌋Un⋆

-- Theorem 6.
thm₆ : ∀ {Γ A} → (M M′ : Γ ⊢ A) → M ≅ M′ → nf M ≡ nf M′
thm₆ M M′ p = cor₁ M M′ (cong⟦ p ⟧Eq id⊩Un⋆)