```------------------------------------------------------------------------
-- Parallel substitutions (defined as functions)
------------------------------------------------------------------------

open import Universe

module deBruijn.Substitution.Function.Basics
{i u e} {Uni : Indexed-universe i u e} where

import deBruijn.Context; open deBruijn.Context Uni
open import Function using (id; _∘_; _\$_)
open import Level using (_⊔_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open P.≡-Reasoning

-- Substitutions, represented as functions from variables to terms.

Sub : ∀ {t} (T : Term-like t) {Γ Δ : Ctxt} → Γ ⇨̂ Δ → Set _
Sub T = [ Var ⟶ T ]

private
module Dummy {t} {T : Term-like t} where

open Term-like T

-- Interpretation of substitutions: context morphisms.

⟦_⟧⇨ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → Γ ⇨̂ Δ
⟦_⟧⇨ {ρ̂ = ρ̂} _ = ρ̂

-- Application of substitutions to types.

infixl 8 _/I_ _/_

_/I_ : ∀ {Γ Δ i} {ρ̂ : Γ ⇨̂ Δ} → IType Γ i → Sub T ρ̂ → IType Δ i
σ /I ρ = σ /̂I ⟦ ρ ⟧⇨

_/_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Type Γ → Sub T ρ̂ → Type Δ
σ / ρ = σ /̂ ⟦ ρ ⟧⇨

-- Application of substitutions to values.

infixl 8 _/Val_

_/Val_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} →
Value Γ σ → Sub T ρ̂ → Value Δ (σ /̂ ρ̂)
v /Val ρ = v /̂Val ⟦ ρ ⟧⇨

-- Application of substitutions to context extensions.

infixl 8 _/⁺_ _/₊_

_/⁺_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Ctxt⁺ Γ → Sub T ρ̂ → Ctxt⁺ Δ
Γ⁺ /⁺ ρ = Γ⁺ /̂⁺ ⟦ ρ ⟧⇨

_/₊_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Ctxt₊ Γ → Sub T ρ̂ → Ctxt₊ Δ
Γ₊ /₊ ρ = Γ₊ /̂₊ ⟦ ρ ⟧⇨

-- Application of substitutions to variables.

infixl 8 _/∋_ _/∋-lemma_

_/∋_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} → Γ ∋ σ → (ρ : Sub T ρ̂) → Δ ⊢ σ / ρ
x /∋ ρ = ρ · x

_/∋-lemma_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} (x : Γ ∋ σ) (ρ : Sub T ρ̂) →
x /̂∋ ⟦ ρ ⟧⇨ ≅-Value ⟦ x /∋ ρ ⟧
x /∋-lemma ρ = corresponds ρ x

app∋ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Sub T ρ̂ → [ Var ⟶ T ] ρ̂
app∋ ρ = record
{ function    = λ _ x → x /∋       ρ
; corresponds = λ _ x → x /∋-lemma ρ
}

-- Empty substitution.

ε⇨ : ∀ {Δ} → Sub T ε̂[ Δ ]
ε⇨ = record { function = λ _ (); corresponds = λ _ () }

ε⇨[_] : ∀ Δ → Sub T ε̂[ Δ ]
ε⇨[ _ ] = ε⇨

-- Extends a substitution with another term.

private

-- This function is not local to _▻⇨[_]_ because a proof below
-- fails to type check if the function depends on the proof
-- component of the substitution.

fun : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} →
(∀ {τ} → Γ ∋ τ → Δ ⊢ τ /̂ ρ̂) →
(t : Δ ⊢ σ /̂ ρ̂) →
∀ {τ} → Γ ▻ σ ∋ τ → Δ ⊢ τ /̂ (ρ̂ ▻̂ ⟦ t ⟧)
fun f t zero    = t
fun f t (suc x) = f x

infixl 5 _▻⇨_ _▻⇨[_]_

_▻⇨[_]_ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ}
(ρ : Sub T ρ̂) σ (t : Δ ⊢ σ / ρ) → Sub T (ρ̂ ▻̂[ σ ] ⟦ t ⟧)
_▻⇨[_]_ {Γ} {Δ} {ρ̂} ρ σ t =
record { function = λ _ → fun (_·_ ρ) t; corresponds = λ _ → corr }
where
abstract
corr : ∀ {τ} (x : Γ ▻ σ ∋ τ) →
x /̂∋ (ρ̂ ▻̂ ⟦ t ⟧) ≅-Value ⟦ fun (_·_ ρ) t x ⟧
corr zero    = P.refl
corr (suc x) = x /∋-lemma ρ

_▻⇨_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ}
(ρ : Sub T ρ̂) (t : Δ ⊢ σ / ρ) → Sub T (ρ̂ ▻̂[ σ ] ⟦ t ⟧)
ρ ▻⇨ t = ρ ▻⇨[ _ ] t

-- The tail of a nonempty substitution.

tail : ∀ {Γ Δ σ} {ρ̂ : Γ ▻ σ ⇨̂ Δ} → Sub T ρ̂ → Sub T (t̂ail ρ̂)
tail ρ = ρ [∘] weaken∋

-- The head of a nonempty substitution.

head : ∀ {Γ Δ σ} {ρ̂ : Γ ▻ σ ⇨̂ Δ} (ρ : Sub T ρ̂) → Δ ⊢ σ / tail ρ
head ρ = zero /∋ ρ

head-lemma : ∀ {Γ Δ σ} {ρ̂ : Γ ▻ σ ⇨̂ Δ} (ρ : Sub T ρ̂) →
head-lemma ρ = zero /∋-lemma ρ

-- Equality of substitutions.

infix 4 _≅-⇨_

_≅-⇨_ : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} (ρ₁ : Sub T ρ̂₁)
{Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} (ρ₂ : Sub T ρ̂₂) → Set _
_≅-⇨_ = _≅-⟶_

-- Certain uses of substitutivity can be removed.

drop-subst-Sub :
∀ {a} {A : Set a} {x₁ x₂ : A} {Γ Δ}
(f : A → Γ ⇨̂ Δ) {ρ} (eq : x₁ ≡ x₂) →
P.subst (λ x → Sub T (f x)) eq ρ ≅-⇨ ρ
drop-subst-Sub f P.refl = [ P.refl ]

-- Some congruence lemmas.

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

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

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

/I-cong :
∀ {i}
{Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {σ₁ : IType Γ₁ i} {ρ₁ : Sub T ρ̂₁}
{Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {σ₂ : IType Γ₂ i} {ρ₂ : Sub T ρ̂₂} →
σ₁ ≅-IType σ₂ → ρ₁ ≅-⇨ ρ₂ → σ₁ /I ρ₁ ≅-IType σ₂ /I ρ₂
/I-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] = P.refl

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

/⁺-cong : ∀ {Γ₁ Δ₁ Γ⁺₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
{Γ₂ Δ₂ Γ⁺₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
Γ⁺₁ ≅-Ctxt⁺ Γ⁺₂ → ρ₁ ≅-⇨ ρ₂ → Γ⁺₁ /⁺ ρ₁ ≅-Ctxt⁺ Γ⁺₂ /⁺ ρ₂
/⁺-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] = P.refl

/₊-cong : ∀ {Γ₁ Δ₁ Γ₊₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
{Γ₂ Δ₂ Γ₊₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
Γ₊₁ ≅-Ctxt₊ Γ₊₂ → ρ₁ ≅-⇨ ρ₂ → Γ₊₁ /₊ ρ₁ ≅-Ctxt₊ Γ₊₂ /₊ ρ₂
/₊-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] = P.refl

/∋-cong : ∀ {Γ₁ Δ₁ σ₁} {x₁ : Γ₁ ∋ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
{Γ₂ Δ₂ σ₂} {x₂ : Γ₂ ∋ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
x₁ ≅-∋ x₂ → ρ₁ ≅-⇨ ρ₂ → x₁ /∋ ρ₁ ≅-⊢ x₂ /∋ ρ₂
/∋-cong {ρ₁ = _ , _} {ρ₂ = ._ , _} P.refl [ P.refl ] = P.refl

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

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

abstract

-- Some eta-laws, based on the assumption of extensionality.

-- Eta in empty contexts.

ηε : P.Extensionality (i ⊔ u ⊔ e) (i ⊔ u ⊔ e ⊔ t) →
∀ {Δ} {ρ̂ : ε ⇨̂ Δ} (ρ : Sub T ρ̂) → ρ ≅-⇨ ε⇨[ Δ ]
ηε ext ρ = extensional-equality₁ ext P.refl (λ ())

-- Eta in non-empty contexts.

η▻ : P.Extensionality (i ⊔ u ⊔ e) (i ⊔ u ⊔ e ⊔ t) →
∀ {Γ Δ σ} {ρ̂ : Γ ▻ σ ⇨̂ Δ} (ρ : Sub T ρ̂) →
ρ ≅-⇨ tail ρ ▻⇨[ σ ] head ρ
η▻ ext {Γ} {σ = σ} {ρ̂} ρ = extensional-equality₂ ext lemma₁ lemma₂
where
open Term-like Var using () renaming (_≅-⊢_ to _≅-∋′_)

lemma₁ : ρ̂ ≅-⇨̂ t̂ail ρ̂ ▻̂[ σ ] ⟦ head ρ ⟧
lemma₁ = begin
[ ρ̂                   ]  ≡⟨ P.refl ⟩
[ t̂ail ρ̂ ▻̂ ĥead ρ̂     ]  ≡⟨ ▻̂-cong P.refl P.refl (head-lemma ρ) ⟩
[ t̂ail ρ̂ ▻̂ ⟦ head ρ ⟧ ]  ∎

lemma₂′ : ∀ {τ} (x : Γ ▻ σ ∋ τ) →
x /∋ ρ ≅-⊢ x /∋ (tail ρ ▻⇨[ σ ] head ρ)
lemma₂′ zero    = P.refl
lemma₂′ (suc x) = P.refl

lemma₂ : ∀ {τ₁} {x₁ : Γ ▻ σ ∋ τ₁}
{τ₂} {x₂ : Γ ▻ σ ∋ τ₂} →
x₁ ≅-∋′ x₂ → x₁ /∋ ρ ≅-⊢ x₂ /∋ (tail ρ ▻⇨[ σ ] head ρ)
lemma₂ {x₁ = x} P.refl = lemma₂′ x

-- Two substitutions are equal if their indices are equal and
-- their projections are pairwise equal (assuming extensionality).

extensionality :
P.Extensionality (i ⊔ u ⊔ e) (i ⊔ u ⊔ e ⊔ t) →
∀ {Γ Δ₁} {ρ̂₁ : Γ ⇨̂ Δ₁} {ρ₁ : Sub T ρ̂₁}
{Δ₂} {ρ̂₂ : Γ ⇨̂ Δ₂} {ρ₂ : Sub T ρ̂₂} →
Δ₁ ≅-Ctxt Δ₂ → (∀ {σ} (x : Γ ∋ σ) → x /∋ ρ₁ ≅-⊢ x /∋ ρ₂) →
ρ₁ ≅-⇨ ρ₂
extensionality ext {ε} {ρ₁ = ρ₁} {ρ₂ = ρ₂} P.refl hyp =
ρ₁  ≅-⟶⟨ ηε ext ρ₁ ⟩
ε⇨  ≅-⟶⟨ sym-⟶ \$ ηε ext ρ₂ ⟩
ρ₂  ∎-⟶
extensionality ext {Γ ▻ σ} {ρ₁ = ρ₁} {ρ₂ = ρ₂} P.refl hyp =
ρ₁                  ≅-⟶⟨ η▻ ext ρ₁ ⟩
tail ρ₁ ▻⇨ head ρ₁  ≅-⟶⟨ ▻⇨-cong P.refl
(extensionality ext P.refl (hyp ∘ suc))
(hyp zero) ⟩
tail ρ₂ ▻⇨ head ρ₂  ≅-⟶⟨ sym-⟶ \$ η▻ ext ρ₂ ⟩
ρ₂                  ∎-⟶

open Dummy public
```