deBruijn.Substitution.Function.Simple

------------------------------------------------------------------------
-- Some simple substitution combinators
------------------------------------------------------------------------

-- Given a term type which supports weakening and transformation of
-- variables to terms various substitutions are defined and various
-- lemmas proved.

open import Data.Universe.Indexed

module deBruijn.Substitution.Function.Simple
  {i u e} {Uni : IndexedUniverse i u e} where

import deBruijn.Context; open deBruijn.Context Uni
open import deBruijn.Substitution.Function.Basics
open import deBruijn.Substitution.Function.Map
open import Function as F using (_$_)
open import Level using (_⊔_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open P.≡-Reasoning

-- Simple substitutions.

record Simple {t} (T : Term-like t) : Set (i ⊔ u ⊔ e ⊔ t) where

  open Term-like T

  field

    -- Weakens terms.
    weaken : ∀ {Γ} {σ : Type Γ} → [ T ⟶ T ] ŵk[ σ ]

  -- A synonym.

  weaken[_] : ∀ {Γ} (σ : Type Γ) → [ T ⟶ T ] ŵk[ σ ]
  weaken[_] _ = weaken

  field

    -- Takes variables to terms.
    var : [ Var ⟶⁼ T ]

    -- A property relating weaken and var.
    weaken-var : ∀ {Γ σ τ} (x : Γ ∋ τ) →
                 weaken[ σ ] · (var · x) ≅-⊢ var · suc[ σ ] x

  -- Weakens substitutions.

  wk-subst : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → Sub T (ρ̂ ∘̂ ŵk[ σ ])
  wk-subst ρ = map weaken ρ

  wk-subst[_] : ∀ {Γ Δ} σ {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → Sub T (ρ̂ ∘̂ ŵk[ σ ])
  wk-subst[ _ ] = wk-subst

  -- N-ary weakening of substitutions.

  wk-subst⁺ : ∀ {Γ Δ} Δ⁺ {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → Sub T (ρ̂ ∘̂ ŵk⁺ Δ⁺)
  wk-subst⁺ ε        ρ = ρ
  wk-subst⁺ (Δ⁺ ▻ σ) ρ = wk-subst (wk-subst⁺ Δ⁺ ρ)

  wk-subst₊ : ∀ {Γ Δ} Δ₊ {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → Sub T (ρ̂ ∘̂ ŵk₊ Δ₊)
  wk-subst₊ ε        ρ = ρ
  wk-subst₊ (σ ◅ Δ₊) ρ = wk-subst₊ Δ₊ (wk-subst ρ)

  -- Lifting.

  infixl 10 _↑_
  infix  10 _↑

  _↑_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → ∀ σ → Sub T (ρ̂ ↑̂ σ)
  ρ ↑ _ =
    P.subst (Sub T)
            (≅-⇨̂-⇒-≡ $ ▻̂-cong P.refl P.refl
                         (P.sym $ corresponds var zero))
            (wk-subst ρ ▻⇨ var · zero)

  _↑ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → Sub T (ρ̂ ↑̂ σ)
  ρ ↑ = ρ ↑ _

  -- N-ary lifting.

  infixl 10 _↑⁺_ _↑₊_

  _↑⁺_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → ∀ Γ⁺ → Sub T (ρ̂ ↑̂⁺ Γ⁺)
  ρ ↑⁺ ε        = ρ
  ρ ↑⁺ (Γ⁺ ▻ σ) = (ρ ↑⁺ Γ⁺) ↑

  _↑₊_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → ∀ Γ₊ → Sub T (ρ̂ ↑̂₊ Γ₊)
  ρ ↑₊ ε        = ρ
  ρ ↑₊ (σ ◅ Γ₊) = ρ ↑ ↑₊ Γ₊

  -- The identity substitution.

  id[_] : ∀ Γ → Sub T îd[ Γ ]
  id[ ε     ] = ε⇨
  id[ Γ ▻ σ ] = id[ Γ ] ↑

  id : ∀ {Γ} → Sub T îd[ Γ ]
  id = id[ _ ]

  -- N-ary weakening.

  wk⁺ : ∀ {Γ} (Γ⁺ : Ctxt⁺ Γ) → Sub T (ŵk⁺ Γ⁺)
  wk⁺ ε        = id
  wk⁺ (Γ⁺ ▻ σ) = wk-subst (wk⁺ Γ⁺)

  wk₊ : ∀ {Γ} (Γ₊ : Ctxt₊ Γ) → Sub T (ŵk₊ Γ₊)
  wk₊ Γ₊ = wk-subst₊ Γ₊ id

  -- Weakening.

  wk[_] : ∀ {Γ} (σ : Type Γ) → Sub T ŵk[ σ ]
  wk[ σ ] = wk⁺ (ε ▻ σ)

  wk : ∀ {Γ} {σ : Type Γ} → Sub T ŵk[ σ ]
  wk = wk[ _ ]

  private

    -- Three possible definitions of wk coincide definitionally.

    coincide₁ : ∀ {Γ} {σ : Type Γ} → wk⁺ (ε ▻ σ) ≡ wk₊ (σ ◅ ε)
    coincide₁ = P.refl

    coincide₂ : ∀ {Γ} {σ : Type Γ} → wk⁺ (ε ▻ σ) ≡ wk-subst id
    coincide₂ = P.refl

  -- A substitution which only replaces the first variable.

  sub : ∀ {Γ σ} (t : Γ ⊢ σ) → Sub T (ŝub ⟦ t ⟧)
  sub t = id ▻⇨ t

  abstract

    -- Unfolding lemma for _↑.

    unfold-↑ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂) →
               ρ ↑ σ ≅-⇨ wk-subst[ σ / ρ ] ρ ▻⇨[ σ ] var · zero
    unfold-↑ _ =
      drop-subst-Sub F.id
        (≅-⇨̂-⇒-≡ $ ▻̂-cong P.refl P.refl (P.sym $ corresponds var zero))

  -- Some congruence lemmas.

  weaken-cong : ∀ {Γ₁ σ₁ τ₁} {t₁ : Γ₁ ⊢ τ₁}
                  {Γ₂ σ₂ τ₂} {t₂ : Γ₂ ⊢ τ₂} →
                σ₁ ≅-Type σ₂ → t₁ ≅-⊢ t₂ →
                weaken[ σ₁ ] · t₁ ≅-⊢ weaken[ σ₂ ] · t₂
  weaken-cong P.refl P.refl = P.refl

  var-cong : ∀ {Γ₁ σ₁} {x₁ : Γ₁ ∋ σ₁}
               {Γ₂ σ₂} {x₂ : Γ₂ ∋ σ₂} →
               x₁ ≅-∋ x₂ → var · x₁ ≅-⊢ var · x₂
  var-cong P.refl = P.refl

  wk-subst-cong : ∀ {Γ₁ Δ₁ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
                    {Γ₂ Δ₂ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
                  σ₁ ≅-Type σ₂ → ρ₁ ≅-⇨ ρ₂ →
                  wk-subst[ σ₁ ] ρ₁ ≅-⇨ wk-subst[ σ₂ ] ρ₂
  wk-subst-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] =
    [ P.refl ]

  abstract

    wk-subst⁺-cong : ∀ {Γ₁ Δ₁ Γ⁺₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
                       {Γ₂ Δ₂ Γ⁺₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
                     Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → ρ₁ ≅-⇨ ρ₂ →
                     wk-subst⁺ Γ⁺₁ ρ₁ ≅-⇨ wk-subst⁺ Γ⁺₂ ρ₂
    wk-subst⁺-cong {Γ⁺₁ = ε} {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] =
      [ P.refl ]
    wk-subst⁺-cong {Γ⁺₁ = Γ⁺₁ ▻ σ} P.refl ρ₁≅ρ₂ =
      wk-subst-cong (P.refl {x = [ σ ]})
                    (wk-subst⁺-cong (P.refl {x = [ Γ⁺₁ ]}) ρ₁≅ρ₂)

    wk-subst₊-cong : ∀ {Γ₁ Δ₁ Γ₊₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
                       {Γ₂ Δ₂ Γ₊₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
                     Γ₊₁ ≅-Ctxt₊ Γ₊₂ → ρ₁ ≅-⇨ ρ₂ →
                     wk-subst₊ Γ₊₁ ρ₁ ≅-⇨ wk-subst₊ Γ₊₂ ρ₂
    wk-subst₊-cong {Γ₊₁ = ε} {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] =
      [ P.refl ]
    wk-subst₊-cong {Γ₊₁ = σ ◅ Γ₊₁} P.refl ρ₁≅ρ₂ =
      wk-subst₊-cong (P.refl {x = [ Γ₊₁ ]}) (wk-subst-cong P.refl ρ₁≅ρ₂)

    ↑-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁} {σ₁}
               {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} {σ₂} →
             ρ₁ ≅-⇨ ρ₂ → σ₁ ≅-Type σ₂ → ρ₁ ↑ σ₁ ≅-⇨ ρ₂ ↑ σ₂
    ↑-cong {ρ₁ = ρ₁} {σ₁} {ρ₂ = ρ₂} {σ₂} ρ₁≅ρ₂ σ₁≅σ₂ =
      let lemma = /-cong σ₁≅σ₂ ρ₁≅ρ₂ in
      ρ₁ ↑ σ₁                               ≅-⟶⟨ unfold-↑ ρ₁ ⟩
      wk-subst ρ₁ ▻⇨ var · zero[ σ₁ / ρ₁ ]  ≅-⟶⟨ ▻⇨-cong σ₁≅σ₂ (wk-subst-cong lemma ρ₁≅ρ₂) (var-cong (zero-cong lemma)) ⟩
      wk-subst ρ₂ ▻⇨ var · zero[ σ₂ / ρ₂ ]  ≅-⟶⟨ sym-⟶ $ unfold-↑ ρ₂ ⟩
      ρ₂ ↑ σ₂                               ∎-⟶

    ↑⁺-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁} {Γ⁺₁}
                {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} {Γ⁺₂} →
              ρ₁ ≅-⇨ ρ₂ → Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → ρ₁ ↑⁺ Γ⁺₁ ≅-⇨ ρ₂ ↑⁺ Γ⁺₂
    ↑⁺-cong {ρ₁ = _ , _} {Γ⁺₁ = ε} {ρ₂ = ._ , _} [ P.refl ] P.refl =
      [ P.refl ]
    ↑⁺-cong {Γ⁺₁ = Γ⁺ ▻ σ} ρ₁≅ρ₂ P.refl =
      ↑-cong (↑⁺-cong ρ₁≅ρ₂ (P.refl {x = [ Γ⁺ ]})) P.refl

    ↑₊-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁} {Γ₊₁}
                {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} {Γ₊₂} →
              ρ₁ ≅-⇨ ρ₂ → Γ₊₁ ≅-Ctxt₊ Γ₊₂ → ρ₁ ↑₊ Γ₊₁ ≅-⇨ ρ₂ ↑₊ Γ₊₂
    ↑₊-cong {ρ₁ = _ , _} {Γ₊₁ = ε} {ρ₂ = ._ , _} [ P.refl ] P.refl =
      [ P.refl ]
    ↑₊-cong {Γ₊₁ = σ ◅ Γ₊} ρ₁≅ρ₂ P.refl =
      ↑₊-cong (↑-cong ρ₁≅ρ₂ P.refl) (P.refl {x = [ Γ₊ ]})

  id-cong : ∀ {Γ₁ Γ₂} → Γ₁ ≅-Ctxt Γ₂ → id[ Γ₁ ] ≅-⇨ id[ Γ₂ ]
  id-cong P.refl = [ P.refl ]

  wk⁺-cong : ∀ {Γ₁} {Γ⁺₁ : Ctxt⁺ Γ₁} {Γ₂} {Γ⁺₂ : Ctxt⁺ Γ₂} →
             Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → wk⁺ Γ⁺₁ ≅-⇨ wk⁺ Γ⁺₂
  wk⁺-cong P.refl = [ P.refl ]

  wk₊-cong : ∀ {Γ₁} {Γ₊₁ : Ctxt₊ Γ₁} {Γ₂} {Γ₊₂ : Ctxt₊ Γ₂} →
             Γ₊₁ ≅-Ctxt₊ Γ₊₂ → wk₊ Γ₊₁ ≅-⇨ wk₊ Γ₊₂
  wk₊-cong P.refl = [ P.refl ]

  wk-cong : ∀ {Γ₁} {σ₁ : Type Γ₁} {Γ₂} {σ₂ : Type Γ₂} →
            σ₁ ≅-Type σ₂ → wk[ σ₁ ] ≅-⇨ wk[ σ₂ ]
  wk-cong P.refl = [ P.refl ]

  sub-cong : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ σ₁} {Γ₂ σ₂} {t₂ : Γ₂ ⊢ σ₂} →
             t₁ ≅-⊢ t₂ → sub t₁ ≅-⇨ sub t₂
  sub-cong P.refl = [ P.refl ]

  abstract

    -- Some lemmas relating variables to lifting.

    /∋-↑ : ∀ {Γ Δ σ τ} {ρ̂ : Γ ⇨̂ Δ} (x : Γ ▻ σ ∋ τ) (ρ : Sub T ρ̂) →
           x /∋ ρ ↑ ≅-⊢ x /∋ (wk-subst[ σ / ρ ] ρ ▻⇨ var · zero)
    /∋-↑ x ρ = /∋-cong (P.refl {x = [ x ]}) (unfold-↑ ρ)

    zero-/∋-↑ : ∀ {Γ Δ} σ {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂) →
                zero[ σ ] /∋ ρ ↑ ≅-⊢ var · zero[ σ / ρ ]
    zero-/∋-↑ σ ρ = begin
      [ zero[ σ ] /∋ ρ ↑                        ]  ≡⟨ /∋-↑ zero[ σ ] ρ ⟩
      [ zero[ σ ] /∋ (wk-subst ρ ▻⇨ var · zero) ]  ≡⟨ P.refl ⟩
      [ var · zero                              ]  ∎

    suc-/∋-↑ : ∀ {Γ Δ τ} σ {ρ̂ : Γ ⇨̂ Δ} (x : Γ ∋ τ) (ρ : Sub T ρ̂) →
               suc[ σ ] x /∋ ρ ↑ ≅-⊢ x /∋ wk-subst[ σ / ρ ] ρ
    suc-/∋-↑ σ x ρ = begin
      [ suc[ σ ] x /∋ ρ ↑                        ]  ≡⟨ /∋-↑ (suc[ σ ] x) ρ ⟩
      [ suc[ σ ] x /∋ (wk-subst ρ ▻⇨ var · zero) ]  ≡⟨ P.refl ⟩
      [ x /∋ wk-subst ρ                          ]  ∎

  -- One can weaken either before or after looking up a variable.
  -- (Note that this lemma holds definitionally, unlike the
  -- corresponding lemma in deBruijn.Substitution.Data.Simple.)

  /∋-wk-subst : ∀ {Γ Δ σ τ} {ρ̂ : Γ ⇨̂ Δ} (x : Γ ∋ τ) (ρ : Sub T ρ̂) →
                x /∋ wk-subst[ σ ] ρ ≅-⊢ weaken[ σ ] · (x /∋ ρ)
  /∋-wk-subst x ρ = P.refl

  abstract

    -- A corollary.

    /∋-wk-subst-var :
      ∀ {Γ Δ σ τ} {ρ̂ : Γ ⇨̂ Δ}
      (ρ : Sub T ρ̂) (x : Γ ∋ τ) (y : Δ ∋ τ / ρ) →
      x /∋               ρ ≅-⊢ var ·          y →
      x /∋ wk-subst[ σ ] ρ ≅-⊢ var · suc[ σ ] y
    /∋-wk-subst-var ρ x y hyp = begin
      [ x /∋ wk-subst ρ    ]  ≡⟨ P.refl ⟩
      [ weaken · (x /∋ ρ)  ]  ≡⟨ weaken-cong P.refl hyp ⟩
      [ weaken · (var · y) ]  ≡⟨ weaken-var y ⟩
      [ var · suc y        ]  ∎

    -- The identity substitution has no effect.

    /-id : ∀ {Γ} (σ : Type Γ) → σ / id ≅-Type σ
    /-id σ = P.refl

    /⁺-id : ∀ {Γ} (Γ⁺ : Ctxt⁺ Γ) → Γ⁺ /⁺ id ≅-Ctxt⁺ Γ⁺
    /⁺-id Γ⁺ = begin
      [ Γ⁺ /⁺ id ]  ≡⟨ P.refl ⟩
      [ Γ⁺ /̂⁺ îd ]  ≡⟨ /̂⁺-îd Γ⁺ ⟩
      [ Γ⁺       ]  ∎

    /₊-id : ∀ {Γ} (Γ₊ : Ctxt₊ Γ) → Γ₊ /₊ id ≅-Ctxt₊ Γ₊
    /₊-id Γ₊ = begin
      [ Γ₊ /₊ id ]  ≡⟨ P.refl ⟩
      [ Γ₊ /̂₊ îd ]  ≡⟨ /̂₊-îd Γ₊ ⟩
      [ Γ₊       ]  ∎

    mutual

      /∋-id : ∀ {Γ σ} (x : Γ ∋ σ) → x /∋ id ≅-⊢ var · x
      /∋-id {Γ = ε}     ()
      /∋-id {Γ = Γ ▻ σ} x = begin
        [ x /∋ id ↑               ]  ≡⟨ /∋-↑ x id ⟩
        [ x /∋ (wk ▻⇨ var · zero) ]  ≡⟨ lemma x ⟩
        [ var · x                 ]  ∎
        where
        lemma : ∀ {τ} (x : Γ ▻ σ ∋ τ) →
                x /∋ (wk[ σ ] ▻⇨ var · zero) ≅-⊢ var · x
        lemma zero    = P.refl
        lemma (suc x) = /∋-wk x

      -- Weakening a variable is equivalent to incrementing it.

      /∋-wk : ∀ {Γ σ τ} (x : Γ ∋ τ) →
              x /∋ wk[ σ ] ≅-⊢ var · suc[ σ ] x
      /∋-wk x = /∋-wk-subst-var id x x (/∋-id x)

    -- The n-ary lifting of the identity substitution is the identity
    -- substitution.

    id-↑⁺ : ∀ {Γ} (Γ⁺ : Ctxt⁺ Γ) → id ↑⁺ Γ⁺ ≅-⇨ id[ Γ ++⁺ Γ⁺ ]
    id-↑⁺ ε        = id ∎-⟶
    id-↑⁺ (Γ⁺ ▻ σ) =
      (id ↑⁺ Γ⁺) ↑  ≅-⟶⟨ ↑-cong (id-↑⁺ Γ⁺) P.refl ⟩
      id ↑          ∎-⟶

    id-↑₊ : ∀ {Γ} (Γ₊ : Ctxt₊ Γ) → id ↑₊ Γ₊ ≅-⇨ id[ Γ ++₊ Γ₊ ]
    id-↑₊ ε        = id ∎-⟶
    id-↑₊ (σ ◅ Γ₊) =
      id ↑ ↑₊ Γ₊  ≅-⟶⟨ [ P.refl ] ⟩
      id   ↑₊ Γ₊  ≅-⟶⟨ id-↑₊ Γ₊ ⟩
      id          ∎-⟶

    -- The identity substitution has no effect even if lifted.

    /∋-id-↑⁺ : ∀ {Γ} Γ⁺ {σ} (x : Γ ++⁺ Γ⁺ ∋ σ) →
               x /∋ id ↑⁺ Γ⁺ ≅-⊢ var · x
    /∋-id-↑⁺ Γ⁺ x = begin
      [ x /∋ id ↑⁺ Γ⁺ ]  ≡⟨ /∋-cong (P.refl {x = [ x ]}) (id-↑⁺ Γ⁺) ⟩
      [ x /∋ id       ]  ≡⟨ /∋-id x ⟩
      [ var · x       ]  ∎

    /∋-id-↑₊ : ∀ {Γ} Γ₊ {σ} (x : Γ ++₊ Γ₊ ∋ σ) →
               x /∋ id ↑₊ Γ₊ ≅-⊢ var · x
    /∋-id-↑₊ Γ₊ x = begin
      [ x /∋ id ↑₊ Γ₊ ]  ≡⟨ /∋-cong (P.refl {x = [ x ]}) (id-↑₊ Γ₊) ⟩
      [ x /∋ id       ]  ≡⟨ /∋-id x ⟩
      [ var · x       ]  ∎

    -- If ρ is morally a renaming, then "deep application" of ρ to a
    -- variable is still a variable.

    /∋-↑⁺ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ}
            (ρ : Sub T ρ̂) (f : [ Var ⟶ Var ] ρ̂) →
            (∀ {σ} (x : Γ ∋ σ) → x /∋ ρ ≅-⊢ var · (f · x)) →
            ∀ Γ⁺ {σ} (x : Γ ++⁺ Γ⁺ ∋ σ) →
            x /∋ ρ ↑⁺ Γ⁺ ≅-⊢ var · (lift f Γ⁺ · x)
    /∋-↑⁺ ρ f hyp ε        x    = hyp x
    /∋-↑⁺ ρ f hyp (Γ⁺ ▻ σ) zero = begin
      [ zero[ σ ] /∋ (ρ ↑⁺ Γ⁺) ↑ ]  ≡⟨ zero-/∋-↑ σ (ρ ↑⁺ Γ⁺) ⟩
      [ var · zero               ]  ∎
    /∋-↑⁺ ρ f hyp (Γ⁺ ▻ σ) (suc x) = begin
      [ suc[ σ ] x /∋ (ρ ↑⁺ Γ⁺) ↑        ]  ≡⟨ suc-/∋-↑ σ x (ρ ↑⁺ Γ⁺) ⟩
      [ x /∋ wk-subst (ρ ↑⁺ Γ⁺)          ]  ≡⟨ P.refl ⟩
      [ weaken · (x /∋ ρ ↑⁺ Γ⁺)          ]  ≡⟨ weaken-cong P.refl (/∋-↑⁺ ρ f hyp Γ⁺ x) ⟩
      [ weaken · (var · (lift f Γ⁺ · x)) ]  ≡⟨ weaken-var (lift f Γ⁺ · x) ⟩
      [ var · suc (lift f Γ⁺ · x)        ]  ∎

    -- "Deep weakening" of a variable can be expressed without
    -- reference to the weaken function.

    /∋-wk-↑⁺ : ∀ {Γ σ} Γ⁺ {τ} (x : Γ ++⁺ Γ⁺ ∋ τ) →
               x /∋ wk[ σ ] ↑⁺ Γ⁺ ≅-⊢
               var · (lift weaken∋[ σ ] Γ⁺ · x)
    /∋-wk-↑⁺ = /∋-↑⁺ wk weaken∋ /∋-wk

    /∋-wk-↑⁺-↑⁺ : ∀ {Γ σ} Γ⁺ Γ⁺⁺ {τ} (x : Γ ++⁺ Γ⁺ ++⁺ Γ⁺⁺ ∋ τ) →
                  x /∋ wk[ σ ] ↑⁺ Γ⁺ ↑⁺ Γ⁺⁺ ≅-⊢
                  var · (lift (lift weaken∋[ σ ] Γ⁺) Γ⁺⁺ · x)
    /∋-wk-↑⁺-↑⁺ Γ⁺ = /∋-↑⁺ (wk ↑⁺ Γ⁺) (lift weaken∋ Γ⁺) (/∋-wk-↑⁺ Γ⁺)

    -- Two n-ary liftings can be merged into one.

    ↑⁺-⁺++⁺ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂) Γ⁺ Γ⁺⁺ →
              ρ ↑⁺ (Γ⁺ ⁺++⁺ Γ⁺⁺) ≅-⇨ ρ ↑⁺ Γ⁺ ↑⁺ Γ⁺⁺
    ↑⁺-⁺++⁺ ρ Γ⁺ ε         = ρ ↑⁺ Γ⁺ ∎-⟶
    ↑⁺-⁺++⁺ ρ Γ⁺ (Γ⁺⁺ ▻ σ) =
      (ρ ↑⁺ (Γ⁺ ⁺++⁺ Γ⁺⁺)) ↑  ≅-⟶⟨ ↑-cong (↑⁺-⁺++⁺ ρ Γ⁺ Γ⁺⁺)
                                          (drop-subst-Type F.id (++⁺-++⁺ Γ⁺ Γ⁺⁺)) ⟩
      (ρ ↑⁺ Γ⁺ ↑⁺ Γ⁺⁺) ↑      ∎-⟶

    ↑₊-₊++₊ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂) Γ₊ Γ₊₊ →
              ρ ↑₊ (Γ₊ ₊++₊ Γ₊₊) ≅-⇨ ρ ↑₊ Γ₊ ↑₊ Γ₊₊
    ↑₊-₊++₊ ρ ε        Γ₊₊ = ρ ↑₊ Γ₊₊ ∎-⟶
    ↑₊-₊++₊ ρ (σ ◅ Γ₊) Γ₊₊ =
      ρ ↑ ↑₊ (Γ₊ ₊++₊ Γ₊₊)  ≅-⟶⟨ ↑₊-₊++₊ (ρ ↑) Γ₊ Γ₊₊ ⟩
      ρ ↑ ↑₊ Γ₊ ↑₊ Γ₊₊      ∎-⟶