{-|
This module defines intrinsically well-typed terms and substitutions for λ○▷pat
as described in sections 3.2, 3.3, and 6.1.
It also defines renaming operations for terms and substitutions.

The definitions follow the style used in the DeBruijn section of
the PLFA book, with the exception that substitutions are defined as a concrete 
data type rather than as functions.
-}

{-# OPTIONS --safe #-}
module Pat.Term where

open import Data.Nat using (ℕ; suc; zero; _≥‴_; ≤‴-refl; ≤‴-step)
open import Function using (id; _∘_)

open import Pat.Context

data Term : (n : ℕ) → Context n → Type n → Set
infix 4 Term
syntax Term n Γ A = Γ ⊢ A ^ n

-- Substitution

infix 4 _⊩_
infix 4 _⊩[_⊢_^_]
infix 4 _∣_⊩_↝_
infix 4 _∣_⊩[_⊢_^_]↝_
infixl 5 _,_
infixl 5 _++ˢ_

{-|
Intrinsically well-typed substitution entries.

Constructors:
  term - An entry whose right-hand side is a term (rule S-Subst).
  var - An entry whose right-hand side is a variable (rule S-Rename).
-}
data _⊩[_⊢_^_] Γ′ {m} (Δ : Context m) (A : Type m) (m≥n : m ≥‴ n) : Set where
  term
    : (e : Γ′ ↾≥ m≥n ++ Δ ⊢ A ^ m)
      ----------------------------
    → Γ′ ⊩[ Δ ⊢ A ^ m≥n ]
  var
    : (x : Γ′ ∋[ Δ ⊢ A ^ m≥n ])
      -------------------------
    → Γ′ ⊩[ Δ ⊢ A ^ m≥n ]

{-|
Intrinsically well-typed substitutions.

Constructors:
  ∅ - The empty substitution.
  _,_ - Add an entry to a substitution.
  _++ˢ_ - Concatenate two substitutions.
-}
data _⊩_ (Γ′ : Context n) : Context n → Set where
  ∅ : Γ′ ⊩ ∅
  _,_ :  (σ : Γ′ ⊩ Γ) → (item : Γ′ ⊩[ Δ ⊢ A ^ m≥n ]) → Γ′ ⊩ Γ ,[ Δ ⊢ A ^ m≥n ]
  _++ˢ_ : Γ′ ⊩ Γ₁ → Γ′ ⊩ Γ₂ →  Γ′ ⊩ Γ₁ ++ Γ₂

-- | Lookup a substitution by a variable (debruijn index).
lookup : Γ′ ⊩ Γ → Γ ∋[ Δ ⊢ A ^ m≥n ] → Γ′ ⊩[ Δ ⊢ A ^ m≥n ]
lookup (σ , e) Z = e
lookup (σ , e) (S x) = lookup σ x
lookup (σ₁ ++ˢ σ₂) (L x) = lookup σ₁ x
lookup (σ₁ ++ˢ σ₂) (R x) = lookup σ₂ x

-- | Turn a function from variables to substitution entries into a substitution.
lookup⁻¹ : (f : ∀ {m} {Δ} {A} {m≥n : m ≥‴ _} → Γ ∋[ Δ ⊢ A ^ m≥n ] → Γ′ ⊩[ Δ ⊢ A ^ m≥n ]) → Γ′ ⊩ Γ
lookup⁻¹ {Γ = ∅} f = ∅
lookup⁻¹ {Γ = Γ ,[ _ ⊢ _ ^ _ ]} f = lookup⁻¹ (f ∘ S) , f Z
lookup⁻¹ {Γ = Γ₁ ++ Γ₂} f = lookup⁻¹ (f ∘ L) ++ˢ lookup⁻¹ (f ∘ R)

-- | Concatenate two substitutions, flattening the _++ˢ_ constructors in the second argument.
infixl 5 _++ˢ♭_
_++ˢ♭_ : Γ′ ⊩ Γ → Γ′ ⊩ Δ →  Γ′ ⊩ Γ ++♭ Δ
σ₁ ++ˢ♭ ∅ = σ₁
σ₁ ++ˢ♭ (σ₂ , item) = σ₁ ++ˢ♭ σ₂ , item
σ₁ ++ˢ♭ (σ₂ ++ˢ σ₃) = σ₁ ++ˢ♭ σ₂ ++ˢ♭ σ₃

-- | Flipped version of the _⊩_ type.
Subst : Context n → Context n → Set
Subst Γ Γ′ = Γ′ ⊩ Γ

-- Patterns
variable
  Π Π′ Π₁ Π₂ Π₃ : Context n

infix 4 Pattern
syntax Pattern n Γ Δ A Π = Γ ∣ Δ ⊢ A ^ n ↝ Π
data Pattern : (n : ℕ) → Context n → Context n → Type n → Context n → Set

{-|
Intrinsically well-typed substitution pattern entries.
Constructors:
  term - An entry whose right-hand side is a pattern (rule P-S-Subst).
  var - An entry whose right-hand side is a variable (rule P-S-Rename).
-}
data _∣_⊩[_⊢_^_]↝_ (Γ′ Δ : Context n) {m} (Δ′ : Context m) (A : Type m) (m≥n : m ≥‴ n) : (Π : Context m) → Set where
  term
    : (p : Γ′ ↾≥ m≥n ∣ Δ ↾≥ m≥n ++ Δ′ ⊢ A ^ m ↝ Π)
      --------------------------------------------
    → Γ′ ∣ Δ ⊩[ Δ′ ⊢ A ^ m≥n ]↝ Π
  var
    : (x : Γ′ ++ Δ ∋[ Δ′ ⊢ A ^ m≥n ])
      -------------------------------
    → Γ′ ∣ Δ ⊩[ Δ′ ⊢ A ^ m≥n ]↝ ∅

{-|
Intrinsically well-typed substitution patterns.

Constructors:
  ∅ - The empty substitution pattern.
  _,_ - Add an entry to a substitution pattern.
  _++ˢᵖ_ - Concatenate two substitution patterns.
-}
data _∣_⊩_↝_ (Γ′ : Context n) (Δ : Context n) : Context n → (Π : Context n) → Set where
  ∅ : Γ′ ∣ Δ ⊩ ∅ ↝ ∅
  _,_
    : (π : Γ′ ∣ Δ ⊩ Γ ↝ Π₁)
    → (item :  Γ′ ∣ Δ ⊩[ Δ′ ⊢ A ^ m≥n ]↝ Π₂)
      ---------------------------------------------------
    → Γ′ ∣ Δ ⊩ Γ ,[ Δ′ ⊢ A ^ m≥n ] ↝ Π₁ ++♭ inject≥ m≥n Π₂
  _++ˢᵖ_
    : (π₁ : Γ′ ∣ Δ ⊩ Γ ↝ Π₁)
    → (π₂ : Γ′ ∣ Δ ⊩ Δ′ ↝ Π₂)
      -------------------------------
    → Γ′ ∣ Δ ⊩ Γ ++ Δ′ ↝ Π₁ ++♭ Π₂

-- Pattern definition
-- We use the "flattening" version _++♭_ of the concatenation operator
-- to make sure that the list of pattern variables does not depend on the term structure.
data Pattern where
  -- | Rule P-PVar
  `pat
      --------------------------------------
    : Γ ∣ Δ ⊢ A ^ n ↝ ∅ ,[ Δ ⊢ A ^ ≤‴-refl ]

  -- | Rule P-VarSubst1
  `_`with₁_
    : (x : Γ ∋[ Δ′ ⊢ A ^ ≤‴-refl ])
    → (σ : Γ ++ Δ ⊩ Δ′)
      -------------------------------
    → Γ ∣ Δ ⊢ A ^ n ↝ ∅

  -- | Rule P-VarSubst2
  `_`with₂_
    : (x : Δ ∋[ Δ′ ⊢ A ^ ≤‴-refl ])
    → (π : Γ ∣ Δ ⊩ Δ′ ↝ Π)
      -------------------------------
    → Γ ∣ Δ ⊢ A ^ n ↝ Π

  -- | Rule P-True
  `true
      ---------------------
    : Γ ∣ Δ ⊢ `Bool ^ n ↝ ∅

  -- | Rule P-False
  `false
      ---------------------
    : Γ ∣ Δ ⊢ `Bool ^ n ↝ ∅

  -- | Rule P-If
  `if_`then_`else_
    : (p₁ : Γ ∣ Δ ⊢ `Bool ^ n ↝ Π₁)
    → (p₂ : Γ ∣ Δ ⊢ A ^ n ↝ Π₂)
    → (p₃ : Γ ∣ Δ ⊢ A ^ n ↝ Π₃)
      ------------------------------
    → Γ ∣ Δ ⊢ A ^ n ↝ Π₁ ++♭ Π₂ ++♭ Π₃

  -- | Rule P-CtxAbs
  `λ⟨_⟩_
    : ∀ Δ′
    → (p : Γ ∣ Δ ,[ inject₁ Δ′ ⊢ A ^ ≤‴-refl ] ⊢ B ^ n ↝ Π)
      -----------------------------------
    → Γ ∣ Δ ⊢ [ Δ′ ⊢ A ]⇒ B ^ n ↝ Π

  -- | Rule P-CtxApp
  _·_
    : (p₁ : Γ ∣ Δ ⊢ [ Δ′ ⊢ A ]⇒ B ^ n ↝ Π₁)
    → (p₂ : Γ ∣ Δ ++ inject₁ Δ′ ⊢ A ^ n ↝ Π₂)
      -------------------------
    → Γ ∣ Δ ⊢ B ^ n ↝ Π₁ ++♭ Π₂

  -- | Rule P-Quote
  ⟨_⟩
    : (p : Γ ↾ ∣ Δ ↾ ⊢ A ^ suc n ↝ Π)
      -------------------------------
    → Γ ∣ Δ ⊢ ◯ A ^ n ↝ inject₁ Π

  -- | Rule P-LetQuote
  `let⟨_⟩
    : ∀ Δ′
    → (p₁ : Γ ∣ Δ ++ inject₁ Δ′ ⊢ ◯ A ^ n ↝ Π₁)
    → (p₂ : Γ ∣ Δ ,[ Δ′ ⊢ A ^ ≤‴-step ≤‴-refl ] ⊢ B ^ n ↝ Π₂)
      ------------------------------------------------
    → Γ ∣ Δ ⊢ B ^ n ↝ Π₁ ++♭ Π₂

  -- | Rule P-Wrap
  `wrap : ∀ Δ′
    → (e : Γ ∣ Δ ++ inject₁ Δ′ ⊢ A ^ n ↝ Π)
      ----------------------
    → Γ ∣ Δ ⊢ Δ′ ▷ A ^ n ↝ Π

  -- | Rule P-LetWrap
  `letwrap : ∀ Δ′
    → (e₁ : Γ ∣ Δ ⊢ Δ′ ▷ A ^ n ↝ Π₁)
    → (e₂ : Γ ∣ Δ ,[ inject₁ Δ′ ⊢ A ^ ≤‴-refl ] ⊢ B ^ n ↝ Π₂)
      --------------------------------------
    → Γ ∣ Δ ⊢ B ^ n ↝ Π₁ ++♭ Π₂

  -- | Rule P-IfLet
  `iflet⟨_⟩
    : ∀ Δ′
    → (p : Γ ↾ ++ (Δ ↾) ∣ Δ′ ⊢ A ^ suc n ↝ Π)
    → (p₁ : Γ ∣ Δ ++ inject₁ Δ′ ⊢ ◯ A ^ n ↝ Π₁)
    → (p₂ : Γ ∣ Δ ++ inject₁ Π ⊢ B ^ n ↝ Π₂)
    → (p₃ : Γ ∣ Δ ⊢ B ^ n ↝ Π₃)
      ------------------------------------------------
    → Γ ∣ Δ ⊢ B ^ n ↝ Π₁ ++♭ Π₂ ++♭ Π₃

  -- | Rule P-Rewrite
  `rewrite
    : (p₁ : Γ ∣ Δ ⊢ ◯ A ^ n ↝ Π₁)
    → (p : Γ ↾ ++ (Δ ↾) ∣ ∅ ⊢ B ^ suc n ↝ Π)
    → (p₂ : Γ ∣ Δ ++ inject₁ Π ⊢ ◯ B ^ n ↝ Π₂)
      ----------------------
    → Γ ∣ Δ ⊢ ◯ A ^ n ↝ Π₁ ++♭ Π₂

-- Term definition

infix 5 `λ⟨_⟩_
infixl 7 _·_
infixr 7 `if_`then_`else_
infix 9 `_`with_

{-|
Intrinsically well-typed terms.
Each constructor corresponds to a rule in the type system.
-}
data Term where
  -- | Rule VarSubst
  `_`with_
    : (x : Γ ∋[ Δ ⊢ A ^ ≤‴-refl ])
    → (σ : Γ ⊩ Δ)
      ----------------------
    → Γ ⊢ A ^ n

  -- | Rule True
  `true
      --------------
    : Γ ⊢ `Bool ^ n

  -- | Rule False
  `false
      --------------
    : Γ ⊢ `Bool ^ n

  -- | Rule If
  `if_`then_`else_
    : (e₁ : Γ ⊢ `Bool ^ n)
    → (e₂ : Γ ⊢ A ^ n)
    → (e₃ : Γ ⊢ A ^ n)
      --------------
    → Γ ⊢ A ^ n

  -- | Rule CtxAbs
  `λ⟨_⟩_
    : ∀ Δ
    → (e : Γ ,[ inject₁ Δ ⊢ A ^ ≤‴-refl ] ⊢ B ^ n)
      ---------------------------
    → Γ ⊢ [ Δ ⊢ A ]⇒ B ^ n

  -- | Rule CtxApp
  _·_
    : (e₁ : Γ ⊢ [ Δ ⊢ A ]⇒ B ^ n)
    → (e₂ : Γ ++ inject₁ Δ ⊢ A ^ n)
      -------------
    → Γ ⊢ B ^ n

  -- | Rule Quote
  ⟨_⟩
    : (e : Γ ↾ ⊢ A ^ suc n)
      -------------
    → Γ ⊢ ◯ A ^ n

  -- | Rule LetQuote
  `let⟨_⟩ : ∀ Δ
    → (e₁ : Γ ++ inject₁ Δ ⊢ ◯ A ^ n)
    → (e₂ : Γ ,[ Δ ⊢ A ^ ≤‴-step ≤‴-refl ] ⊢ B ^ n)
      --------------------------------------
    → Γ ⊢ B ^ n

  -- | Rule Wrap
  `wrap : ∀ Δ
    → (e : Γ ++ inject₁ Δ ⊢ A ^ n)
      ----------------------
    → Γ ⊢ Δ ▷ A ^ n
  
  -- | Rule LetWrap
  `letwrap : ∀ Δ
    → (e₁ : Γ ⊢ Δ ▷ A ^ n)
    → (e₂ : Γ ,[ inject₁ Δ ⊢ A ^ ≤‴-refl ] ⊢ B ^ n)
      --------------------------------------
    → Γ ⊢ B ^ n

  -- | Rule IfLet
  `iflet⟨_⟩ : ∀ Δ
    → (p : Γ ↾ ∣ Δ ⊢ A ^ suc n ↝ Π)
    → (e₁ : Γ ++ inject₁ Δ ⊢ ◯ A ^ n)
    → (e₂ : Γ ++ inject₁ Π ⊢ B ^ n)
    → (e₃ : Γ ⊢ B ^ n)
      --------------------------------------
    → Γ ⊢ B ^ n

  -- | Rule Rewrite
  `rewrite
    : (e₁ : Γ ⊢ ◯ A ^ n)
    → (p : Γ ↾ ∣ ∅ ⊢ B ^ suc n ↝ Π)
    → (e₂ : Γ ++ inject₁ Π ⊢ ◯ B ^ n)
      ----------------------
    → Γ ⊢ ◯ A ^ n

-- Renaming

-- | Rename a term.
rename : Rename Γ Γ′ → Γ ⊢ A ^ n → Γ′ ⊢ A ^ n
-- | Rename a substitution.
renameSubst : Rename Γ Γ′ → Γ ⊩ Δ → Γ′ ⊩ Δ
-- | Rename a substitution entry.
renameSubstItem : Rename Γ Γ′ → Γ ⊩[ Δ ⊢ A ^ m≥n ] → Γ′ ⊩[ Δ ⊢ A ^ m≥n ]
-- | Rename a pattern.
renamePattern : Rename Γ Γ′ → Γ ∣ Δ ⊢ A ^ n ↝ Π → Γ′ ∣ Δ ⊢ A ^ n ↝ Π
-- | Rename a substitution pattern.
renameSubstPattern : Rename Γ Γ′ → Γ ∣ Δ ⊩ Δ′ ↝ Π → Γ′ ∣ Δ ⊩ Δ′ ↝ Π
-- | Rename a substitution pattern entry.
renameSubstPatternItem : Rename Γ Γ′ → Γ ∣ Δ ⊩[ Δ′ ⊢ A ^ m≥n ]↝ Π → Γ′ ∣ Δ ⊩[ Δ′ ⊢ A ^ m≥n ]↝ Π

rename ρ (` x `with σ) = ` ρ x `with renameSubst ρ σ
rename ρ `true = `true
rename ρ `false = `false
rename ρ (`if e₁ `then e₂ `else e₃) = `if rename ρ e₁ `then rename ρ e₂ `else rename ρ e₃
rename ρ (`λ⟨ Δ ⟩ e) = `λ⟨ Δ ⟩ (rename (ext ρ) e)
rename ρ (e₁ · e₂) = rename ρ e₁ · rename (ext++ _ ρ) e₂
rename ρ ⟨ e ⟩ = ⟨ rename (ext↾ ρ) e ⟩
rename ρ (`let⟨ Δ ⟩ e₁ e₂) = `let⟨ Δ ⟩ (rename (ext++ (inject₁ Δ) ρ) e₁) (rename (ext ρ) e₂)
rename ρ (`iflet⟨ Δ ⟩ p e₁ e₂ e₃) = `iflet⟨ Δ ⟩ (renamePattern (ext↾ ρ) p) (rename (ext++ (inject₁ Δ) ρ) e₁) (rename (ext++ (inject₁ _) ρ) e₂) (rename ρ e₃)
rename ρ (`wrap Δ e) = `wrap Δ (rename (ext++ (inject₁ Δ) ρ) e)
rename ρ (`letwrap Δ e₁ e₂) = `letwrap Δ (rename ρ e₁) (rename (ext ρ) e₂)
rename ρ (`rewrite e₁ p e₂) = `rewrite (rename ρ e₁) (renamePattern (ext↾ ρ) p)  (rename (ext++ _ ρ) e₂)

renameSubst ρ ∅ = ∅   
renameSubst ρ (σ , item) = renameSubst ρ σ , renameSubstItem ρ item
renameSubst ρ (σ₁ ++ˢ σ₂) = renameSubst ρ σ₁ ++ˢ renameSubst ρ σ₂

renameSubstItem {Δ = Δ} {m≥n = m≥n} ρ (term e) = term (rename (ext++ Δ (ext↾≥ m≥n ρ)) e)
renameSubstItem ρ (var x) = var (ρ x)

renamePattern ρ `pat = `pat
renamePattern ρ (` x `with₁ σ) = ` ρ x `with₁ renameSubst (ext++ _ ρ) σ
renamePattern ρ (` x `with₂ π) = ` x `with₂ renameSubstPattern ρ π
renamePattern ρ `true = `true
renamePattern ρ `false = `false
renamePattern ρ (`if p₁ `then p₂ `else p₃)
  = `if (renamePattern ρ p₁) `then (renamePattern ρ p₂) `else (renamePattern ρ p₃)
renamePattern ρ (`λ⟨ Δ′ ⟩ p) = `λ⟨ Δ′ ⟩ renamePattern ρ p
renamePattern ρ (p₁ · p₂) = renamePattern ρ p₁ · renamePattern ρ p₂
renamePattern ρ (⟨ p ⟩) = ⟨ renamePattern (ext↾ ρ) p ⟩
renamePattern ρ (`let⟨ Δ ⟩ p₁ p₂) = `let⟨ Δ ⟩ (renamePattern ρ p₁) (renamePattern ρ p₂)
renamePattern ρ (`iflet⟨ Δ′ ⟩ p e₁ e₂ e₃) = `iflet⟨ Δ′ ⟩ (renamePattern (ext++ _ (ext↾ ρ)) p) (renamePattern ρ e₁) (renamePattern ρ e₂) (renamePattern ρ e₃)
renamePattern ρ (`wrap Δ p) = `wrap Δ (renamePattern ρ p)
renamePattern ρ (`letwrap Δ p₁ p₂) = `letwrap Δ (renamePattern ρ p₁) (renamePattern ρ p₂)
renamePattern ρ (`rewrite e₁ p e₂) = `rewrite (renamePattern ρ e₁) (renamePattern (ext++ _ (ext↾ ρ)) p) (renamePattern ρ e₂)

renameSubstPattern ρ ∅ = ∅
renameSubstPattern ρ (π , item) = renameSubstPattern ρ π , renameSubstPatternItem ρ item
renameSubstPattern ρ (π₁ ++ˢᵖ π₂) = renameSubstPattern ρ π₁ ++ˢᵖ renameSubstPattern ρ π₂

renameSubstPatternItem {m≥n = m≥n} ρ (term p) = term (renamePattern (ext↾≥ m≥n ρ) p)
renameSubstPatternItem ρ (var x) = var ((ext++ _ ρ) x)

-- | Pre-compose a renaming function before a substitution.
renameSubstʳ : Rename Δ′ Δ → Γ ⊩ Δ → Γ ⊩ Δ′
renameSubstʳ ρ σ = lookup⁻¹ (lookup σ ∘ ρ)
 
-- | Lift a renaming funtion to a substitution.
lift : Rename Γ Γ′ → Subst Γ Γ′
lift ρ = lookup⁻¹ (var ∘ ρ)

-- | Extend a substitution by an identity entry.
exts : Subst Γ Γ′ → Subst (Γ ,[ Δ ⊢ A ^ m≥n ]) (Γ′ ,[ Δ ⊢ A ^ m≥n ])
exts {Δ = Δ} {m≥n = m≥n} σ = renameSubst S σ , var Z

-- | Extend a substitution by multiple identity entries (id_Δ)
exts++ : ∀ Δ → Subst Γ Γ′ → Subst (Γ ++ Δ) (Γ′ ++ Δ)
exts++ Δ σ = renameSubst L σ ++ˢ lift R

-- | Eliminate _↾ from _⊩[_⊢_^_].
⊩[]-↾⁻ : Γ ↾ ⊩[ Δ ⊢ A ^ m≥n ] → Γ ⊩[ Δ ⊢ A ^ ≤‴-step m≥n ]
⊩[]-↾⁻ (term e) = term e
⊩[]-↾⁻ (var x) = var (∋-↾⁻ x)

-- | Introduce _↾ into _⊩[_⊢_^_].
⊩[]-↾⁺ : Γ ⊩[ Δ ⊢ A ^ ≤‴-step m≥n ] → Γ ↾ ⊩[ Δ ⊢ A ^ m≥n ]
⊩[]-↾⁺ (term e) = term e
⊩[]-↾⁺ (var x) = var (∋-↾⁺ x)

-- | Restrict a substitution by removing entries at level n.
exts↾ : Subst Γ Γ′ → Subst (Γ ↾) (Γ′ ↾) 
exts↾ ∅ = ∅
exts↾ (_,_ {m≥n = ≤‴-refl} σ item) = exts↾ σ
exts↾ (_,_ {m≥n = ≤‴-step m≥n} σ item) = exts↾ σ , ⊩[]-↾⁺ item
exts↾ (σ₁ ++ˢ σ₂) = exts↾ σ₁ ++ˢ exts↾ σ₂

-- | Restrict a substitution by removing entries below level m.
exts↾≥ : (m≥n : m ≥‴ n) → Subst Γ Γ′ → Subst (Γ ↾≥ m≥n) (Γ′ ↾≥ m≥n)
exts↾≥ ≤‴-refl σ = σ   
exts↾≥ (≤‴-step sm≥n) σ = exts↾≥ sm≥n (exts↾ σ)

-- | Eliminate _↾ from the left of _⊩_ and introduce inject₁ into the right.
⊩-↾⁻ : Γ ↾ ⊩ Δ → Γ ⊩ inject₁ Δ
⊩-↾⁻ ∅ = ∅
⊩-↾⁻ (σ , item) = ⊩-↾⁻ σ , ⊩[]-↾⁻ item
⊩-↾⁻ (σ₁ ++ˢ σ₂) = ⊩-↾⁻ σ₁ ++ˢ ⊩-↾⁻ σ₂
 
-- | Eliminate inject₁ from the right of _⊩_ and introduce _↾ into the left.
⊩-↾⁺ : Γ ⊩ inject₁ Δ → Γ ↾ ⊩ Δ
⊩-↾⁺ {Δ = ∅} ∅ = ∅
⊩-↾⁺ {Δ = Δ ,[ _ ^ _ ]} (σ , item) = ⊩-↾⁺ σ , ⊩[]-↾⁺ item
⊩-↾⁺ {Δ = Δ₁ ++ Δ₂} (σ₁ ++ˢ σ₂) = ⊩-↾⁺ σ₁ ++ˢ ⊩-↾⁺ σ₂

-- | Eliminate _↾≥_ from the left of _⊩_ and introduce inject≥ into the right.
⊩-↾≥⁻ : ∀ m≥n → Γ ↾≥ m≥n ⊩ Δ → Γ ⊩ inject≥ m≥n Δ
⊩-↾≥⁻ ≤‴-refl σ = σ
⊩-↾≥⁻ (≤‴-step m≥n) σ = ⊩-↾⁻ (⊩-↾≥⁻ m≥n σ)

-- | Eliminate inject≥ from the right of _⊩_ and introduce _↾≥_ into the left.
⊩-↾≥⁺ : ∀ m≥n → Γ ⊩ inject≥ m≥n Δ → Γ ↾≥ m≥n ⊩ Δ
⊩-↾≥⁺ ≤‴-refl σ = σ 
⊩-↾≥⁺ (≤‴-step m≥n) σ = ⊩-↾≥⁺ m≥n (⊩-↾⁺ σ)

-- | Eliminate inject₁ from _⊩[_⊢_^_].
⊩[]-inject₁⁻ : inject₁ Γ ⊩[ Δ′ ⊢ A ^ ≤‴-step m≥n ] → Γ ⊩[ Δ′ ⊢ A ^ m≥n ] 
⊩[]-inject₁⁻ {Δ′ = Δ′} {m≥n = m≥n} (term e) = term (rename (ext++ Δ′ (ext↾≥ m≥n (∋-inject₁⁻ ∘ ∋-↾⁻))) e)
⊩[]-inject₁⁻ (var x) = var (∋-inject₁⁻ x)

-- | Introduce inject₁ into _⊩[_⊢_^_].
⊩[]-inject₁⁺ : Γ ⊩[ Δ′ ⊢ A ^ m≥n ] → inject₁ Γ ⊩[ Δ′ ⊢ A ^ ≤‴-step m≥n ]
⊩[]-inject₁⁺ {Δ′ = Δ′} {m≥n = m≥n} (term e) = term (rename (ext++ Δ′ (ext↾≥ m≥n (∋-↾⁺ ∘ ∋-inject₁⁺))) e)
⊩[]-inject₁⁺ (var x) = var (∋-inject₁⁺ x)
 
-- | Eliminate inject₁ from both sides of _⊩_.
⊩-inject₁⁻ : inject₁ Γ′ ⊩ inject₁ Γ → Γ′ ⊩ Γ
⊩-inject₁⁻ {Γ = ∅} ∅ = ∅
⊩-inject₁⁻ {Γ = Γ ,[ Δ ⊢ A ^ m≥n ]} (σ , item) = ⊩-inject₁⁻ σ , ⊩[]-inject₁⁻ item
⊩-inject₁⁻ {Γ = Γ ++ Δ} (σ₁ ++ˢ σ₂) = ⊩-inject₁⁻ σ₁ ++ˢ ⊩-inject₁⁻ σ₂

-- | Introduce inject₁ into both sides of _⊩_.
⊩-inject₁⁺ : Γ′ ⊩ Γ → inject₁ Γ′ ⊩ inject₁ Γ
⊩-inject₁⁺ {Γ = ∅} ∅ = ∅ 
⊩-inject₁⁺ {Γ = Γ ,[ Δ ⊢ A ^ m≥n ]} (σ , item) = ⊩-inject₁⁺ σ , ⊩[]-inject₁⁺ item
⊩-inject₁⁺ {Γ = Γ ++ Δ} (σ₁ ++ˢ σ₂) = ⊩-inject₁⁺ σ₁ ++ˢ ⊩-inject₁⁺ σ₂