{-|
This module proves properties of lookup, lifting, and renaming operations.
-}

{-# OPTIONS --safe #-}
module CtxTyp.Term.Properties where

open import Data.Nat using (ℕ; suc; zero; _≥‴_; ≤‴-refl; ≤‴-step)
open import Function using (id; _∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; cong₂)

open import CtxTyp.Context
open import CtxTyp.Term

private module _ where
  cong₃ : ∀ {A B C D : Set} (f : A → B → C → D) {x x′ y y′ z z′} → x ≡ x′ → y ≡ y′ → z ≡ z′ → f x y z ≡ f x′ y′ z′
  cong₃ f refl refl refl = refl

-- Lookup Properties

-- | Two substitutions are equal if their lookups are equal.
lookup-injective-≗ : {σ₁ σ₂ : Γ′ ⊩ Γ} → lookup σ₁ ≗ lookup σ₂ → σ₁ ≡ σ₂
lookup-injective-≗ {σ₁ = ∅} {σ₂ = ∅} σ₁≗ˢσ₂ = refl
lookup-injective-≗ {σ₁ = σ₁ , item₁} {σ₂ = σ₂ , item₂} σ₁≗σ₂ = cong₂ _,_ (lookup-injective-≗ (σ₁≗σ₂ ∘ S)) (σ₁≗σ₂ Z)
lookup-injective-≗ {σ₁ = σ₁ ++ˢ σ₁′} {σ₂ = σ₂ ++ˢ σ₂′} σ₁≗σ₂ = cong₂ _++ˢ_ (lookup-injective-≗ (σ₁≗σ₂ ∘ L)) (lookup-injective-≗ (σ₁≗σ₂ ∘ R))

-- | lookup is a left-inverse of lookup⁻¹.
lookup-lookup⁻¹ : (f : ∀ {m} {Δ} {A} {m≥n : m ≥‴ _} → Γ ∋[ Δ ⊢ A ^ m≥n ] → Γ′ ⊩[ Δ ⊢ A ^ m≥n ]) → lookup (lookup⁻¹ f) ≗ f
lookup-lookup⁻¹ f Z = refl
lookup-lookup⁻¹ f (S x) = lookup-lookup⁻¹ (f ∘ S) x
lookup-lookup⁻¹ f (L x) = lookup-lookup⁻¹ (f ∘ L) x
lookup-lookup⁻¹ f (R x) = lookup-lookup⁻¹ (f ∘ R) x

-- | lookup⁻¹ respects ≗.
lookup⁻¹-resp-≗ : {f g : ∀ {m} {Δ} {A} {m≥n : m ≥‴ _} → Γ ∋[ Δ ⊢ A ^ m≥n ] → Γ′ ⊩[ Δ ⊢ A ^ m≥n ]} → f ≗ g → lookup⁻¹ f ≡ lookup⁻¹ g
lookup⁻¹-resp-≗ {Γ = ∅} f≗g = refl
lookup⁻¹-resp-≗ {Γ = Γ ,[ _ ^ _ ]} f≗g = cong₂ _,_ (lookup⁻¹-resp-≗ (f≗g ∘ S)) (f≗g Z)
lookup⁻¹-resp-≗ {Γ = Γ₁ ++ Γ₂} f≗g = cong₂ _++ˢ_ (lookup⁻¹-resp-≗ (f≗g ∘ L)) (lookup⁻¹-resp-≗ (f≗g ∘ R))

-- | Looking up (S x) in a extended substitution is the same as looking up x in the original substitution renamed by S.
lookup-exts-S : (σ : Γ′ ⊩ Γ) → lookup (exts {Δ = Δ} {A = A} {m≥n = m≥n} σ) ∘ S ≗ lookup (renameSubst S σ)
lookup-exts-S (σ , item) Z = refl
lookup-exts-S (σ , _) (S x) = lookup-exts-S σ x
lookup-exts-S (σ ++ˢ _) (L x) = lookup-exts-S σ x
lookup-exts-S (_ ++ˢ σ) (R x) = lookup-exts-S σ x

-- | Looking up (L x) in an ++-extended substitution is the same as looking up x in the original substitution renamed by L.
lookup-exts++-L : (σ : Γ′ ⊩ Γ) → lookup (exts++ Δ σ) ∘ L ≗ lookup (renameSubst L σ)
lookup-exts++-L (σ , item) Z = refl
lookup-exts++-L (σ , _) (S x) = lookup-exts++-L σ x
lookup-exts++-L (σ ++ˢ _) (L x) = lookup-exts++-L σ x
lookup-exts++-L (_ ++ˢ σ) (R x) = lookup-exts++-L σ x

-- | Express lookup (exts↾ σ) in terms of lookup σ.
lookup-exts↾ : (σ : Γ′ ⊩ Γ) → lookup (exts↾ σ) ≗  ⊩[]-↾⁺ ∘ lookup σ ∘ ∋-↾⁻
lookup-exts↾ {Γ = Γ ,[ Δ ^ ≤‴-refl ]} (σ , _) x = lookup-exts↾ σ x
lookup-exts↾ {Γ = Γ ,[ Δ ^ ≤‴-step m≥n ]} (_ , item) Z = refl
lookup-exts↾ {Γ = Γ ,[ Δ ^ ≤‴-step m≥n ]} (σ , _) (S x) = lookup-exts↾ σ x
lookup-exts↾ {Γ = Γ ++ _} (σ ++ˢ _) (L x) = lookup-exts↾ σ x
lookup-exts↾ {Γ = _ ++ Γ} (_ ++ˢ σ) (R x) = lookup-exts↾ σ x

-- *-resp-≗ Properties

-- | lift respects ≗.
lift-resp-≗ : ∀ {ρ ρ′ : Rename Γ Γ′} → ρ ≗ ρ′ → lift ρ ≡ lift ρ′
lift-resp-≗ ρ≗ρ′ = lookup⁻¹-resp-≗ (cong var ∘ ρ≗ρ′)

-- | rename and renameSubst respect ≗.
rename-resp-≗ : ∀ {ρ ρ′ : Rename Γ Γ′} → ρ ≗ ρ′ → (e : Term n Γ A) → rename ρ e ≡ rename ρ′ e
renameSubst-resp-≗ : ∀ {ρ ρ′ : Rename Γ Γ′} → ρ ≗ ρ′ → (σ : Γ ⊩ Δ) → renameSubst ρ σ ≡ renameSubst ρ′ σ

rename-resp-≗ ρ≗ρ′ (` x `with σ) = cong₂ `_`with_ (ρ≗ρ′ x) (renameSubst-resp-≗ ρ≗ρ′ σ)
rename-resp-≗ ρ≗ρ′ `true = refl
rename-resp-≗ ρ≗ρ′ `false = refl
rename-resp-≗ ρ≗ρ′ (`if e₁ `then e₂ `else e₃) = cong₃ `if_`then_`else_ (rename-resp-≗ ρ≗ρ′ e₁) (rename-resp-≗ ρ≗ρ′ e₂) (rename-resp-≗ ρ≗ρ′ e₃)
rename-resp-≗ ρ≗ρ′ (`λ⟨ Δ ⟩ e) = cong (`λ⟨ Δ ⟩_) (rename-resp-≗ (ext-resp-≗ ρ≗ρ′) e)
rename-resp-≗ ρ≗ρ′ (e₁ · e₂) = cong₂ _·_ (rename-resp-≗ ρ≗ρ′ e₁) (rename-resp-≗ (ext++-resp-≗ _ ρ≗ρ′) e₂)
rename-resp-≗ ρ≗ρ′ ⟨ e ⟩ = cong ⟨_⟩ (rename-resp-≗ (ext↾-resp-≗ ρ≗ρ′) e)
rename-resp-≗ ρ≗ρ′ (`let⟨ Δ ⟩ e₁ e₂) = cong₂ `let⟨ Δ ⟩ (rename-resp-≗ (ext++-resp-≗ (inject₁ Δ) ρ≗ρ′) e₁) (rename-resp-≗ (ext-resp-≗ ρ≗ρ′) e₂)
rename-resp-≗ ρ≗ρ′ (`wrap Δ e) = cong (`wrap Δ) (rename-resp-≗ (ext++-resp-≗ (inject₁ Δ) ρ≗ρ′) e)
rename-resp-≗ ρ≗ρ′ (`letwrap Δ e₁ e₂) = cong₂ (`letwrap Δ) (rename-resp-≗ ρ≗ρ′ e₁) (rename-resp-≗ (ext-resp-≗ ρ≗ρ′) e₂)

renameSubst-resp-≗ ρ≗ρ′ ∅ = refl
renameSubst-resp-≗ ρ≗ρ′ (_,_ {m≥n = m≥n} σ (term e)) = cong₂ _,_ (renameSubst-resp-≗ ρ≗ρ′ σ) (cong term (rename-resp-≗ (ext++-resp-≗ _ (ext↾≥-resp-≗ m≥n ρ≗ρ′)) e))
renameSubst-resp-≗ ρ≗ρ′ (σ , var x) = cong₂ _,_ (renameSubst-resp-≗ ρ≗ρ′ σ) (cong var (ρ≗ρ′ x))
renameSubst-resp-≗ ρ≗ρ′ (σ ++ˢ σ₁) = cong₂ _++ˢ_ (renameSubst-resp-≗ ρ≗ρ′ σ) (renameSubst-resp-≗ ρ≗ρ′ σ₁)

-- | renameSubstʳ respects ≗.
renameSubstʳ-resp-≗ : ∀ {ρ ρ′ : Rename Δ′ Δ} → ρ ≗ ρ′ → (σ : Γ ⊩ Δ) → renameSubstʳ ρ σ ≡ renameSubstʳ ρ′ σ
renameSubstʳ-resp-≗ ρ≗ρ′ σ = lookup⁻¹-resp-≗ λ x → cong (lookup σ) (ρ≗ρ′ x)

-- *-id Properties

-- | rename and renameSubst maps id to id.
rename-id : (e : Term n Γ A) → rename id e ≡ e
renameSubst-id : (σ : Γ ⊩ Δ) → renameSubst id σ ≡ σ

rename-id (` x `with σ) = cong₂ `_`with_ refl (renameSubst-id σ)
rename-id `true = refl
rename-id `false = refl
rename-id (`if e₁ `then e₂ `else e₃) = cong₃ `if_`then_`else_ (rename-id e₁) (rename-id e₂) (rename-id e₃)
rename-id (`λ⟨ Δ ⟩ e) = cong (`λ⟨ Δ ⟩_) (trans (rename-resp-≗ ext-id e) (rename-id e))
rename-id (e₁ · e₂) = cong₂ _·_ (rename-id e₁) (trans (rename-resp-≗ (ext++-id _) e₂) (rename-id e₂))
rename-id {Γ = Γ} ⟨ e ⟩ = cong ⟨_⟩ (trans (rename-resp-≗ (ext↾-id {xs = Γ}) e) (rename-id e))
rename-id (`let⟨ Δ ⟩ e₁ e₂) = cong₂ (`let⟨ Δ ⟩) (trans (rename-resp-≗ (ext++-id _) e₁) (rename-id e₁)) (trans (rename-resp-≗ ext-id e₂) (rename-id e₂))
rename-id (`wrap Δ e) = cong (`wrap Δ) (trans (rename-resp-≗ (ext++-id _) e) (rename-id e))
rename-id (`letwrap Δ e₁ e₂) = cong₂ (`letwrap Δ) (rename-id e₁) (trans (rename-resp-≗ ext-id e₂) (rename-id e₂))

renameSubst-id ∅ = refl
renameSubst-id (_,_ {m≥n = m≥n} σ (term e)) = cong₂ _,_ (renameSubst-id σ) (cong term (trans (rename-resp-≗ (≗-trans (ext++-resp-≗ _ (ext↾≥-id m≥n)) (ext++-id _)) e) (rename-id e)))
renameSubst-id (σ , var x) = cong₂ _,_ (renameSubst-id σ) refl
renameSubst-id (σ₁ ++ˢ σ₂) = cong₂ _++ˢ_ (renameSubst-id σ₁) (renameSubst-id σ₂)

-- | renameSubstʳ maps id to id.
renameSubstʳ-id : (σ : Γ ⊩ Δ) → renameSubstʳ id σ ≡ σ
renameSubstʳ-id σ = lookup-injective-≗ λ x → lookup-lookup⁻¹ (lookup σ) x

-- *-lift Properties

-- | Looking up a lifted renaming function is the same as applying the renaming function to the variable.
lookup-lift : (ρ : Rename Γ Γ′) (x : Γ ∋[ Δ ⊢ A ^ m≥n ]) → lookup (lift ρ) x ≡ var (ρ x)
lookup-lift ρ x = lookup-lookup⁻¹ (var ∘ ρ) x

-- | Renaming a lifted renaming function is the same as composing the renaming functions.
renameSubst-lift : ∀ {Γ″} (ρ′ : Rename Γ′ Γ″) (ρ : Rename Γ Γ′) → renameSubst ρ′ (lift ρ) ≡ lift (ρ′ ∘ ρ)
renameSubst-lift {Γ = ∅} ρ′ ρ = refl
renameSubst-lift {Γ = Γ ,[ _ ^ m≥n ]} ρ′ ρ = cong (_, var _) (renameSubst-lift ρ′ (ρ ∘ S))
renameSubst-lift {Γ = Γ₁ ++ Γ₂} ρ′ ρ = cong₂ _++ˢ_ (renameSubst-lift ρ′ (ρ ∘ L)) (renameSubst-lift ρ′ (ρ ∘ R))

-- | exts commutes with lift.
exts-lift : ∀ (ρ : Rename Γ Γ′) → exts {Δ = Δ} {A = A} {m≥n = m≥n} (lift ρ) ≡ lift (ext ρ)
exts-lift ρ = cong (_, var Z) (renameSubst-lift S ρ)

-- | exts maps lift id to lift id.
exts-lift-id : exts {Δ = Δ} {A = A} {m≥n = m≥n} (lift {Γ = Γ} id) ≡ lift id
exts-lift-id = trans (exts-lift id) (lift-resp-≗ ext-id)

-- | exts++ commutes with lift.
exts++-lift : ∀ Δ (ρ : Rename Γ Γ′) → exts++ Δ (lift ρ) ≡ lift (ext++ Δ ρ)
exts++-lift Δ ρ = cong (_++ˢ lift R) (renameSubst-lift L ρ)

-- | exts↾ commutes with lift.
exts↾-lift : (ρ : Rename Γ Γ′) → exts↾ (lift ρ) ≡ lift (ext↾ ρ) 
exts↾-lift {Γ = ∅} _ = refl
exts↾-lift {Γ = Γ ,[ _ ^ ≤‴-refl ]} ρ = exts↾-lift (ρ  ∘ S)
exts↾-lift {Γ = Γ ,[ _ ^ ≤‴-step m≥n ]} ρ = cong (_, var (∋-↾⁺ (ρ Z))) (exts↾-lift (ρ ∘ S))
exts↾-lift {Γ = Γ₁ ++ Γ₂} ρ = cong₂ _++ˢ_ (exts↾-lift (ρ ∘ L)) (exts↾-lift (ρ ∘ R))

-- | exts↾≥ commutes with lift.
exts↾≥-lift : (m≥n : m ≥‴ n) → (ρ : Rename Γ Γ′) → exts↾≥ m≥n (lift ρ) ≡ lift (ext↾≥ m≥n ρ) 
exts↾≥-lift ≤‴-refl ρ = refl   
exts↾≥-lift (≤‴-step m≥n) ρ = trans (cong (exts↾≥ m≥n) (exts↾-lift ρ)) (exts↾≥-lift m≥n (ext↾ ρ))

-- | ⊩-inject₁⁻ commutes with lift.
⊩-inject₁⁻-lift : {Γ Γ′ : Context (suc n)} (ρ : Rename (inject₁ Γ) (inject₁ Γ′)) → ⊩-inject₁⁻ (lift ρ) ≡ lift (Rename-inject₁⁻ ρ)
⊩-inject₁⁻-lift {Γ = ∅} ρ = refl
⊩-inject₁⁻-lift {Γ = Γ ,[ x ^ m≥n ]} ρ = cong (_, var (∋-inject₁⁻ (ρ Z))) (⊩-inject₁⁻-lift (ρ ∘ S))
⊩-inject₁⁻-lift {Γ = Γ₁ ++ Γ₂} ρ = cong₂ _++ˢ_ (⊩-inject₁⁻-lift (ρ ∘ L)) (⊩-inject₁⁻-lift (ρ ∘ R))
 
-- | ⊩-inject₁⁻ maps lift id to lift id.
⊩-inject₁⁻-lift-id : {Γ : Context (suc n)} → ⊩-inject₁⁻ (lift {Γ = inject₁ Γ} id) ≡ lift id
⊩-inject₁⁻-lift-id = trans (⊩-inject₁⁻-lift id) (lift-resp-≗ Rename-inject₁⁻-id)

-- *-∘ Properties

-- | rename and renameSubst distribute over ∘.
rename-∘ : ∀ {Γ″ Γ′ Γ} (ρ′ : Rename Γ′ Γ″) (ρ : Rename Γ Γ′) (e : Term n Γ A) → rename (ρ′ ∘ ρ) e ≡ rename ρ′ (rename ρ e)
renameSubst-∘ :  ∀ {Γ″ Γ′ Γ} (ρ′ : Rename Γ′ Γ″) (ρ : Rename Γ Γ′) (σ : Γ ⊩ Δ) → renameSubst (ρ′ ∘ ρ) σ ≡ renameSubst ρ′ (renameSubst ρ σ)

rename-∘ ρ′ ρ (` x `with σ) = cong₂ `_`with_ refl (renameSubst-∘ ρ′ ρ σ)
rename-∘ ρ′ ρ `true = refl
rename-∘ ρ′ ρ `false = refl
rename-∘ ρ′ ρ (`if e₁ `then e₂ `else e₃) = cong₃ `if_`then_`else_ (rename-∘ ρ′ ρ e₁) (rename-∘ ρ′ ρ e₂) (rename-∘ ρ′ ρ e₃)
rename-∘ ρ′ ρ (`λ⟨ Δ ⟩ e) = cong (`λ⟨ Δ ⟩_) (trans (rename-resp-≗ (ext-∘ ρ′ ρ) e) (rename-∘ (ext ρ′) (ext ρ) e))
rename-∘ ρ′ ρ (e₁ · e₂) = cong₂ _·_ (rename-∘ ρ′ ρ e₁) (trans (rename-resp-≗ (ext++-∘ _ ρ′ ρ) e₂) (rename-∘ (ext++ _ ρ′) (ext++ _ ρ) e₂))
rename-∘ ρ′ ρ ⟨ e ⟩ = cong ⟨_⟩ (trans (rename-resp-≗ (ext↾-∘ ρ′ ρ) e) (rename-∘ (ext↾ ρ′) (ext↾ ρ) e))
rename-∘ ρ′ ρ (`let⟨ Δ ⟩ e₁ e₂) = cong₂ (`let⟨ Δ ⟩) (trans (rename-resp-≗ (ext++-∘ _ ρ′ ρ) e₁) (rename-∘ (ext++ _ ρ′) (ext++ _ ρ) e₁)) (trans (rename-resp-≗ (ext-∘ ρ′ ρ) e₂) (rename-∘ (ext ρ′) (ext ρ) e₂))
rename-∘ ρ′ ρ (`wrap Δ e) = cong (`wrap Δ) (trans (rename-resp-≗ (ext++-∘ _ ρ′ ρ) e) (rename-∘ (ext++ _ ρ′) (ext++ _ ρ) e))
rename-∘ ρ′ ρ (`letwrap Δ e₁ e₂) = cong₂ (`letwrap Δ) (rename-∘ ρ′ ρ e₁) (trans (rename-resp-≗ (ext-∘ ρ′ ρ) e₂) (rename-∘ (ext ρ′) (ext ρ) e₂))

renameSubst-∘ ρ′ ρ ∅ = refl
renameSubst-∘ ρ′ ρ (_,_ {m≥n = m≥n} σ (term e)) = cong₂ _,_ (renameSubst-∘ ρ′ ρ σ) (cong term (trans (rename-resp-≗ (≗-trans (ext++-resp-≗ _ (ext↾≥-∘ m≥n ρ′ ρ)) (ext++-∘ _ (ext↾≥ m≥n ρ′) (ext↾≥ m≥n ρ))) e) (rename-∘ (ext++ _ (ext↾≥ m≥n ρ′)) (ext++ _ (ext↾≥ m≥n ρ)) e)))
renameSubst-∘ ρ′ ρ (σ , var x) = cong₂ _,_ (renameSubst-∘ ρ′ ρ σ) refl
renameSubst-∘ ρ′ ρ (σ₁ ++ˢ σ₂) = cong₂ _++ˢ_ (renameSubst-∘ ρ′ ρ σ₁) (renameSubst-∘ ρ′ ρ σ₂)

-- | renameSubstʳ distributes over ∘.
renameSubstʳ-∘ : (ρ′ : Rename Δ′ Δ) (ρ : Rename Δ″ Δ′) (σ : Γ ⊩ Δ) → renameSubstʳ (ρ′ ∘ ρ) σ ≡ renameSubstʳ ρ (renameSubstʳ ρ′ σ)
renameSubstʳ-∘ ρ′ ρ σ = lookup⁻¹-resp-≗ λ x → sym (lookup-lookup⁻¹ (lookup σ ∘ ρ′) (ρ x))

-- *-renameSubst Properties

-- | exts distributes over renameSubst.
exts-renameSubst : ∀ {Γ″ Γ′ Γ} (ρ : Rename Γ′ Γ″) (σ : Γ′ ⊩ Γ) → exts {Δ = Δ} {A = A} {m≥n = m≥n} (renameSubst ρ σ) ≡ renameSubst (ext ρ) (exts σ)
exts-renameSubst ρ σ = cong₂ _,_ (trans (sym (renameSubst-∘ S ρ σ)) (renameSubst-∘ (ext ρ) S σ)) refl

-- | exts++ distributes over renameSubst.
exts++-renameSubst : ∀ {Γ″ Γ′ Γ : Context n} Δ (ρ : Rename Γ′ Γ″) (σ : Γ′ ⊩ Γ) → exts++ Δ (renameSubst ρ σ) ≡ renameSubst (ext++ Δ ρ) (exts++ Δ σ)
exts++-renameSubst Δ ρ σ = cong₂ _++ˢ_ (trans (sym (renameSubst-∘ L ρ σ)) (renameSubst-∘ (ext++ Δ ρ) L σ)) (sym (renameSubst-lift (ext++ Δ ρ) R))

-- | exts↾ distributes over renameSubst.
exts↾-renameSubst : ∀ {Γ″ Γ′ Γ : Context n} (ρ : Rename Γ′ Γ″) (σ : Γ′ ⊩ Γ) → exts↾ (renameSubst ρ σ) ≡ renameSubst (ext↾ ρ) (exts↾ σ)
exts↾-renameSubst ρ ∅ = refl 
exts↾-renameSubst ρ (_,_ {m≥n = ≤‴-refl} σ (term e)) = exts↾-renameSubst ρ σ
exts↾-renameSubst ρ (_,_ {m≥n = ≤‴-refl} σ (var x)) = exts↾-renameSubst ρ σ
exts↾-renameSubst ρ (_,_ {m≥n = ≤‴-step m≥n} σ (term e)) = cong₂ _,_ (exts↾-renameSubst ρ σ) refl
exts↾-renameSubst ρ (_,_ {m≥n = ≤‴-step m≥n} σ (var x)) = cong₂ _,_ (exts↾-renameSubst ρ σ) (cong var (sym (ext↾-∋-↾⁺ ρ x)))   
exts↾-renameSubst ρ (σ₁ ++ˢ σ₂) = cong₂ _++ˢ_ (exts↾-renameSubst ρ σ₁) (exts↾-renameSubst ρ σ₂)

-- | exts↾≥ distributes over renameSubst.
exts↾≥-renameSubst : ∀ {Γ″ Γ′ Γ : Context n} (m≥n : m ≥‴ n) (ρ : Rename Γ′ Γ″) (σ : Γ′ ⊩ Γ) → exts↾≥ m≥n (renameSubst ρ σ) ≡ renameSubst (ext↾≥ m≥n ρ) (exts↾≥ m≥n σ)
exts↾≥-renameSubst ≤‴-refl ρ σ = refl
exts↾≥-renameSubst (≤‴-step m≥n) ρ σ = trans (cong (exts↾≥ m≥n) (exts↾-renameSubst ρ σ)) (exts↾≥-renameSubst m≥n (ext↾ ρ) (exts↾ σ))

-- | ⊩-inject₁⁻ distributes over renameSubst.
⊩-inject₁⁻-renameSubst : ∀ {Γ″ Γ′ Γ : Context (suc n)} (ρ : Rename (inject₁ Γ′) (inject₁ Γ″)) (σ : inject₁ Γ′ ⊩ inject₁  Γ) → ⊩-inject₁⁻ (renameSubst ρ σ) ≡ renameSubst (Rename-inject₁⁻ ρ) (⊩-inject₁⁻ σ)
⊩-inject₁⁻-renameSubst {Γ = ∅} ρ ∅ = refl
⊩-inject₁⁻-renameSubst {Γ″ = Γ″} {Γ = Γ ,[ Δ ⊢ A ^ m≥n ]} ρ (σ , term e) = cong₂ _,_ (⊩-inject₁⁻-renameSubst ρ σ) (cong term
  (trans (sym (rename-∘ _ _ e))
    (trans (rename-resp-≗
      (λ {
        (L x) → cong L
          (trans (sym (ext↾≥-∘ m≥n _ _ x))
            (trans (ext↾≥-resp-≗ m≥n (λ x → cong ∋-inject₁⁻
                (trans (∋-↾⁻-∋-↾⁺ (ρ (∋-↾⁻ x))) (cong ρ (sym (∋-inject₁⁺-∋-inject₁⁻ (∋-↾⁻ x)))))) x)
              (ext↾≥-∘ m≥n _ _ x)));
        (R x) → refl }) e)
      (rename-∘ _ _ e))))
⊩-inject₁⁻-renameSubst {Γ = Γ ,[ _ ^ m≥n ]} ρ (σ , var x) = cong₂ _,_ (⊩-inject₁⁻-renameSubst ρ σ) (cong var (cong (∋-inject₁⁻ ∘ ρ) (sym (∋-inject₁⁺-∋-inject₁⁻ x))))
⊩-inject₁⁻-renameSubst {Γ = Γ₁ ++ Γ₂} ρ (σ ++ˢ σ₁) = cong₂ _++ˢ_ (⊩-inject₁⁻-renameSubst ρ σ) (⊩-inject₁⁻-renameSubst ρ σ₁)

-- | lookup commutes with renameSubst.
lookup-renameSubst : ∀ {Γ″ Γ′ Γ} (ρ : Rename Γ′ Γ″) (σ : Γ′ ⊩ Γ) (x : Γ ∋[ Δ ⊢ A ^ m≥n ]) → lookup (renameSubst ρ σ) x ≡ renameSubstItem ρ (lookup σ x)
lookup-renameSubst ρ (σ , item) Z = refl
lookup-renameSubst ρ (σ , _) (S x) = lookup-renameSubst ρ σ x
lookup-renameSubst ρ (σ₁ ++ˢ σ₂) (L x) = lookup-renameSubst ρ σ₁ x
lookup-renameSubst ρ (σ₁ ++ˢ σ₂) (R x) = lookup-renameSubst ρ σ₂ x

-- | lookup distributes over renameSubstʳ.
lookup-renameSubstʳ : ∀ (ρ : Rename Δ′ Δ) (σ : Γ ⊩ Δ) (x : Δ′ ∋[ Δ″ ⊢ A ^ m≥n ]) → lookup (renameSubstʳ ρ σ) x ≡ lookup σ (ρ x)
lookup-renameSubstʳ ρ σ x = lookup-lookup⁻¹ (lookup σ ∘ ρ) x

-- | ⊩-inject₁⁻ commutes with exts++.
⊩-inject₁⁻-exts++ : ∀ {Γ : Context (suc n)} (σ : inject₁ Γ ⊩ inject₁ Δ)  → ⊩-inject₁⁻ (exts++ (inject₁ Δ′) σ) ≡ exts++ Δ′ (⊩-inject₁⁻ σ)
⊩-inject₁⁻-exts++ σ = cong₂ (_++ˢ_)
  (trans (⊩-inject₁⁻-renameSubst L σ) (renameSubst-resp-≗ Rename-inject₁⁻-L (⊩-inject₁⁻ σ)))
  (trans (⊩-inject₁⁻-lift R) (lift-resp-≗ Rename-inject₁⁻-R))

-- | ⊩[]-inject₁⁻ distributes over lookup.
⊩[]-inject₁⁻-lookup
  : ∀ {Γ Δ : Context (suc n)} (σ : inject₁ Γ ⊩ inject₁ Δ) (x : inject₁ Δ ∋[ Δ′ ⊢ A ^ ≤‴-step m≥n ])
  → ⊩[]-inject₁⁻ (lookup σ x) ≡ lookup (⊩-inject₁⁻ σ) (∋-inject₁⁻ x)
⊩[]-inject₁⁻-lookup {Δ = Δ ,[ _ ⊢ _ ^ _ ] } (_ , item) Z = refl
⊩[]-inject₁⁻-lookup {Δ = Δ ,[ _ ⊢ _ ^ _ ] } (σ , _) (S x) = ⊩[]-inject₁⁻-lookup σ x
⊩[]-inject₁⁻-lookup {Δ = Δ ++ _} (σ ++ˢ _) (L x) = ⊩[]-inject₁⁻-lookup σ x
⊩[]-inject₁⁻-lookup {Δ = Δ ++ _} (_ ++ˢ σ) (R x) = ⊩[]-inject₁⁻-lookup σ x

-- | Relating ⊩-inject₁⁻ and exts↾.
⊩-inject₁⁻≡exts↾ : {Γ Δ : Context (suc n)} (σ : inject₁ Γ ⊩ inject₁ Δ) → renameSubstʳ (∋-inject₁⁻ ∘ ∋-↾⁻) (⊩-inject₁⁻ σ) ≡ renameSubst (∋-inject₁⁻ ∘ ∋-↾⁻) (exts↾ σ)
⊩-inject₁⁻≡exts↾ {Δ = ∅} ∅ = refl
⊩-inject₁⁻≡exts↾ {Δ = Δ ,[ Δ′ ⊢ A ^ m≥n ]} (σ , var x) = cong₂ _,_ (⊩-inject₁⁻≡exts↾ σ) (cong (var ∘ ∋-inject₁⁻) (sym (∋-↾⁻-∋-↾⁺ x)))
⊩-inject₁⁻≡exts↾ {Δ = Δ ,[ Δ′ ⊢ A ^ m≥n ]} (σ , term e) = cong₂ _,_ (⊩-inject₁⁻≡exts↾ σ) refl
⊩-inject₁⁻≡exts↾ {Δ = Δ₁ ++ Δ₂ } (σ₁ ++ˢ σ₂) = cong₂ _++ˢ_ (⊩-inject₁⁻≡exts↾ σ₁) (⊩-inject₁⁻≡exts↾ σ₂)
 
-- | Relating ⊩-inject₁⁻ and exts↾ in another way.
⊩-inject₁⁻≡exts↾′ : {Γ Δ : Context (suc n)} (σ : inject₁ Γ ⊩ inject₁ Δ) → ⊩-inject₁⁻ σ ≡ renameSubstʳ (∋-↾⁺ ∘ ∋-inject₁⁺) (renameSubst (∋-inject₁⁻ ∘ ∋-↾⁻) (exts↾ σ))
⊩-inject₁⁻≡exts↾′ σ = trans (trans (trans (sym (renameSubstʳ-id (⊩-inject₁⁻ σ))) (renameSubstʳ-resp-≗ (λ x → sym (∋-inject₁⁻-∋-↾⁻-∋-↾⁺-∋-inject₁⁺ x)) (⊩-inject₁⁻ σ))) (renameSubstʳ-∘ (∋-inject₁⁻ ∘ ∋-↾⁻) (∋-↾⁺ ∘ ∋-inject₁⁺) (⊩-inject₁⁻ σ))) (cong (renameSubstʳ (∋-↾⁺ ∘ ∋-inject₁⁺)) (⊩-inject₁⁻≡exts↾ σ))