```------------------------------------------------------------------------
-- 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.

{-# OPTIONS --universe-polymorphism #-}

open import Universe

module deBruijn.Substitution.Data.Simple
{i u e} {Uni : Indexed-universe i u e} where

import deBruijn.Context; open deBruijn.Context Uni
open import deBruijn.Substitution.Data.Basics
open import deBruijn.Substitution.Data.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 (ρ̂ ↑̂ σ)
ρ ↑ = ρ ↑ _

_↑⋆ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} → Subs T ρ̂ → Subs T (ρ̂ ↑̂ σ)
ε        ↑⋆ = ε
(ρs ▻ ρ) ↑⋆ = ρs ↑⋆ ▻ ρ ↑

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

-- N-ary lifting.

infixl 10 _↑⁺_ _↑⁺⋆_ _↑₊_ _↑₊⋆_

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

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

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

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

-- 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

-- 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

wk-subst⁺-cong : ∀ {Γ₁ Δ₁ Γ⁺₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
{Γ₂ Δ₂ Γ⁺₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → ρ₁ ≅-⇨ ρ₂ →
wk-subst⁺ Γ⁺₁ ρ₁ ≅-⇨ wk-subst⁺ Γ⁺₂ ρ₂
wk-subst⁺-cong P.refl P.refl = P.refl

wk-subst₊-cong : ∀ {Γ₁ Δ₁ Γ₊₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
{Γ₂ Δ₂ Γ₊₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
Γ₊₁ ≅-Ctxt₊ Γ₊₂ → ρ₁ ≅-⇨ ρ₂ →
wk-subst₊ Γ₊₁ ρ₁ ≅-⇨ wk-subst₊ Γ₊₂ ρ₂
wk-subst₊-cong P.refl P.refl = P.refl

↑-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁} {σ₁}
{Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} {σ₂} →
ρ₁ ≅-⇨ ρ₂ → σ₁ ≅-Type σ₂ → ρ₁ ↑ σ₁ ≅-⇨ ρ₂ ↑ σ₂
↑-cong P.refl P.refl = P.refl

↑⋆-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρs₁ : Subs T ρ̂₁} {σ₁}
{Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρs₂ : Subs T ρ̂₂} {σ₂} →
ρs₁ ≅-⇨⋆ ρs₂ → σ₁ ≅-Type σ₂ → ρs₁ ↑⋆ σ₁ ≅-⇨⋆ ρs₂ ↑⋆ σ₂
↑⋆-cong P.refl P.refl = P.refl

↑⁺-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁} {Γ⁺₁}
{Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} {Γ⁺₂} →
ρ₁ ≅-⇨ ρ₂ → Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → ρ₁ ↑⁺ Γ⁺₁ ≅-⇨ ρ₂ ↑⁺ Γ⁺₂
↑⁺-cong P.refl P.refl = P.refl

↑⁺⋆-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρs₁ : Subs T ρ̂₁} {Γ⁺₁}
{Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρs₂ : Subs T ρ̂₂} {Γ⁺₂} →
ρs₁ ≅-⇨⋆ ρs₂ → Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ →
ρs₁ ↑⁺⋆ Γ⁺₁ ≅-⇨⋆ ρs₂ ↑⁺⋆ Γ⁺₂
↑⁺⋆-cong P.refl P.refl = P.refl

↑₊-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁} {Γ₊₁}
{Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} {Γ₊₂} →
ρ₁ ≅-⇨ ρ₂ → Γ₊₁ ≅-Ctxt₊ Γ₊₂ → ρ₁ ↑₊ Γ₊₁ ≅-⇨ ρ₂ ↑₊ Γ₊₂
↑₊-cong P.refl P.refl = P.refl

↑₊⋆-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρs₁ : Subs T ρ̂₁} {Γ₊₁}
{Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρs₂ : Subs T ρ̂₂} {Γ₊₂} →
ρs₁ ≅-⇨⋆ ρs₂ → Γ₊₁ ≅-Ctxt₊ Γ₊₂ →
ρs₁ ↑₊⋆ Γ₊₁ ≅-⇨⋆ ρs₂ ↑₊⋆ Γ₊₂
↑₊⋆-cong P.refl P.refl = P.refl

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

-- 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 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.

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

-- 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 ρ    ]  ≡⟨ /∋-wk-subst x ρ ⟩
[ 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-↑⁺ ε        = P.refl
id-↑⁺ (Γ⁺ ▻ σ) = begin
[ (id ↑⁺ Γ⁺) ↑ ]  ≡⟨ ↑-cong (id-↑⁺ Γ⁺) P.refl ⟩
[ id ↑         ]  ∎

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

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

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

-- 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       ]  ∎

-- N-ary lifting distributes over composition.

▻-↑⁺⋆ : ∀ {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε}
(ρs : Subs T ρ̂₁) (ρ : Sub T ρ̂₂) Γ⁺ →
(ρs ▻ ρ) ↑⁺⋆ Γ⁺ ≅-⇨⋆ ρs ↑⁺⋆ Γ⁺ ▻ ρ ↑⁺ (Γ⁺ /⁺⋆ ρs)
▻-↑⁺⋆ ρs ρ ε        = P.refl
▻-↑⁺⋆ ρs ρ (Γ⁺ ▻ σ) = begin
[ ((ρs ▻ ρ) ↑⁺⋆ Γ⁺) ↑⋆                  ]  ≡⟨ ↑⋆-cong (▻-↑⁺⋆ ρs ρ Γ⁺) P.refl ⟩
[ (ρs ↑⁺⋆ Γ⁺ ▻ ρ ↑⁺ (Γ⁺ /⁺⋆ ρs)) ↑⋆     ]  ≡⟨ P.refl ⟩
[ (ρs ↑⁺⋆ Γ⁺) ↑⋆ ▻ (ρ ↑⁺ (Γ⁺ /⁺⋆ ρs)) ↑ ]  ∎

▻-↑₊⋆ : ∀ {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε}
(ρs : Subs T ρ̂₁) (ρ : Sub T ρ̂₂) Γ₊ →
(ρs ▻ ρ) ↑₊⋆ Γ₊ ≅-⇨⋆ ρs ↑₊⋆ Γ₊ ▻ ρ ↑₊ (Γ₊ /₊⋆ ρs)
▻-↑₊⋆ ρs ρ ε        = P.refl
▻-↑₊⋆ ρs ρ (σ ◅ Γ₊) = begin
[ (ρs ▻ ρ) ↑⋆   ↑₊⋆ Γ₊                     ]  ≡⟨ P.refl ⟩
[ (ρs ↑⋆ ▻ ρ ↑) ↑₊⋆ Γ₊                     ]  ≡⟨ ▻-↑₊⋆ (ρs ↑⋆) (ρ ↑) Γ₊ ⟩
[ ρs ↑₊⋆ (σ ◅ Γ₊) ▻ ρ ↑₊ ((σ ◅ Γ₊) /₊⋆ ρs) ]  ∎

-- 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 (ρ ↑⁺ Γ⁺)          ]  ≡⟨ /∋-wk-subst x (ρ ↑⁺ Γ⁺) ⟩
[ 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 ρ̂) Γ⁺ Γ⁺⁺ →
ρ ↑⁺ (Γ⁺ ⁺++⁺ Γ⁺⁺) ≅-⇨ ρ ↑⁺ Γ⁺ ↑⁺ Γ⁺⁺
↑⁺-⁺++⁺ ρ Γ⁺ ε         = P.refl
↑⁺-⁺++⁺ ρ Γ⁺ (Γ⁺⁺ ▻ σ) = begin
[ (ρ ↑⁺ (Γ⁺ ⁺++⁺ Γ⁺⁺)) ↑ ]  ≡⟨ ↑-cong (↑⁺-⁺++⁺ ρ Γ⁺ Γ⁺⁺)
(drop-subst-Type F.id (++⁺-++⁺ Γ⁺ Γ⁺⁺)) ⟩
[ (ρ ↑⁺ Γ⁺ ↑⁺ Γ⁺⁺) ↑     ]  ∎

↑₊-₊++₊ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρ : Sub T ρ̂) Γ₊ Γ₊₊ →
ρ ↑₊ (Γ₊ ₊++₊ Γ₊₊) ≅-⇨ ρ ↑₊ Γ₊ ↑₊ Γ₊₊
↑₊-₊++₊ ρ ε        Γ₊₊ = P.refl
↑₊-₊++₊ ρ (σ ◅ Γ₊) Γ₊₊ = begin
[ ρ ↑ ↑₊ (Γ₊ ₊++₊ Γ₊₊) ]  ≡⟨ ↑₊-₊++₊ (ρ ↑) Γ₊ Γ₊₊ ⟩
[ ρ ↑ ↑₊ Γ₊ ↑₊ Γ₊₊     ]  ∎
```