module univTypes.SubjectReduction.ConversionProperties where

open import Data.Product renaming (_,_ to ⟨_,_⟩)
open import Data.Sum
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; subst; cong; cong₂; module ≡-Reasoning)
open import Data.Fin using (zero; suc) renaming (Fin to 𝔽)
open import Relation.Nullary using (¬_)
open import Data.Empty using (⊥; ⊥-elim)

open import univTypes.SubjectReduction.Specification
open import univTypes.SubjectReduction.Confluence using (↪ₚ*-trans; ξ*-λ; ξ*-·₁; ξ*-·₂; ξ*-∀₁; ξ*-∀₂; ξ*-subst₁; ξ*-subst₂; ξ*-subst₃)
open import univTypes.SubjectReduction.Confluence using (ξ*-∃₁; ξ*-∃₂; ξ*-,₁; ξ*-,₂; ξ*-≡₁; ξ*-≡₂; ξ*-proj₁; ξ*-proj₂)
open import univTypes.SubjectReduction.Confluence using (confluence; _↪ₚ_; _↪ₚ*_; ↪ₚ-refl; ↪ₚ-ren; ↪ₚ*→↪*; ↪*→↪ₚ*); open _↪ₚ*_; open _↪ₚ_
open import univTypes.SubjectReduction.Composition using (swap-0↦-extᵣ-fusion; swap-0↦-extₛ-fusion)
open import univTypes.Util.Fin

--------------------------------------------------------------------------------

-- Conversion is an equivalence relation

≈-refl : ∀ {n} {e : Term n}
  → e ≈ e
≈-refl = mk-≈ _ ↪*-refl ↪*-refl

≈-sym : ∀ {n} {e₁ e₂ : Term n}
  → e₁ ≈ e₂
  → e₂ ≈ e₁
≈-sym (mk-≈ x y z) = mk-≈ x z y

≈-trans : ∀ {n} {e₁ e₂ e₃ : Term n}
  → e₁ ≈ e₂
  → e₂ ≈ e₃
  → e₁ ≈ e₃
≈-trans (mk-≈ x e₁↪*x e₂↪*x) (mk-≈ y e₂↪*y e₃↪*y) with confluence e₂↪*x e₂↪*y 
... | ⟨ e' , ⟨ x↪*e' , y↪*e' ⟩ ⟩ = mk-≈ e' (↪*-trans e₁↪*x x↪*e') (↪*-trans e₃↪*y y↪*e')  

----------------------------------------------------------------------------

-- Reduction implies conversion

↪→≈ : ∀ {n} {e₁ e₂ : Term n}
  → e₁ ↪ e₂
  → e₁ ≈ e₂
↪→≈ e↪e' = mk-≈ _ (↪*-step e↪e' ↪*-refl) ↪*-refl

--------------------------------------------------------------------------------

-- Congruency rules from parallel reduction, but using ↪* instead of ↪

ξₚ*-λ : ∀ {n} {e e' : Term (suc n)}
  → e ↪ₚ* e'
  ---------------
  → `λ e ↪ₚ* `λ e'
ξₚ*-λ e↪ₚ*e' = ↪*→↪ₚ* (ξ*-λ (↪ₚ*→↪*  e↪ₚ*e'))

ξₚ*-proj₁ : ∀ {n} {e e' : Term n}
  → e ↪ₚ* e'
  ---------------
  → `proj₁ e ↪ₚ* `proj₁ e'
ξₚ*-proj₁ e↪ₚ*e' = ↪*→↪ₚ* (ξ*-proj₁ (↪ₚ*→↪*  e↪ₚ*e'))

ξₚ*-proj₂ : ∀ {n} {e e' : Term n}
  → e ↪ₚ* e'
  ---------------
  → `proj₂ e ↪ₚ* `proj₂ e'

ξₚ*-proj₂ e↪ₚ*e' = ↪*→↪ₚ* (ξ*-proj₂ (↪ₚ*→↪*  e↪ₚ*e'))

ξₚ*-· : ∀ {n} {e₁ e₂ e₁' e₂' : Term n}
  → e₁ ↪ₚ* e₁'
  → e₂ ↪ₚ* e₂'
  ---------------------
  → e₁ · e₂ ↪ₚ* e₁' · e₂'
ξₚ*-· e₁↪ₚ*e₁' e₂↪ₚ*e₂' = ↪ₚ*-trans 
                            (↪*→↪ₚ* (ξ*-·₁ (↪ₚ*→↪*  e₁↪ₚ*e₁')))
                            (↪*→↪ₚ* (ξ*-·₂ (↪ₚ*→↪*  e₂↪ₚ*e₂')))

ξₚ*-, : ∀ {n} {e₁ e₂ e₁' e₂' : Term n}
  → e₁ ↪ₚ* e₁'
  → e₂ ↪ₚ* e₂'
  ---------------------
  → e₁ `, e₂ ↪ₚ* e₁' `, e₂'
ξₚ*-, e₁↪ₚ*e₁' e₂↪ₚ*e₂' = ↪ₚ*-trans 
                            (↪*→↪ₚ* (ξ*-,₁ (↪ₚ*→↪*  e₁↪ₚ*e₁')))
                            (↪*→↪ₚ* (ξ*-,₂ (↪ₚ*→↪*  e₂↪ₚ*e₂')))

ξₚ*-≡ : ∀ {n} {e₁ e₂ e₁' e₂' : Term n}
  → e₁ ↪ₚ* e₁'
  → e₂ ↪ₚ* e₂'
  ---------------------
  → e₁ `≡ e₂ ↪ₚ* e₁' `≡ e₂'
ξₚ*-≡ e₁↪ₚ*e₁' e₂↪ₚ*e₂' = ↪ₚ*-trans 
                            (↪*→↪ₚ* (ξ*-≡₁ (↪ₚ*→↪*  e₁↪ₚ*e₁')))
                            (↪*→↪ₚ* (ξ*-≡₂ (↪ₚ*→↪*  e₂↪ₚ*e₂')))

ξₚ*-∀ : ∀ {n} {t₁ t₁' : Term n} {t₂ t₂' : Term (suc n)}
  → t₁ ↪ₚ* t₁'
  → t₂ ↪ₚ* t₂'
  -------------------------------
  → ∀[x⦂ t₁ ] t₂ ↪ₚ* ∀[x⦂ t₁' ] t₂'
ξₚ*-∀ x↪ₚ*x' t↪ₚ*t' = ↪ₚ*-trans 
                    (↪*→↪ₚ* (ξ*-∀₁ (↪ₚ*→↪* x↪ₚ*x')))
                    (↪*→↪ₚ* (ξ*-∀₂ (↪ₚ*→↪* t↪ₚ*t')))

ξₚ*-∃ : ∀ {n} {t₁ t₁' : Term n} {t₂ t₂' : Term (suc n)}
  → t₁ ↪ₚ* t₁'
  → t₂ ↪ₚ* t₂'
  -------------------------------
  → ∃[x⦂ t₁ ] t₂ ↪ₚ* ∃[x⦂ t₁' ] t₂'
ξₚ*-∃ x↪ₚ*x' t↪ₚ*t' = ↪ₚ*-trans 
                    (↪*→↪ₚ* (ξ*-∃₁ (↪ₚ*→↪* x↪ₚ*x')))
                    (↪*→↪ₚ* (ξ*-∃₂ (↪ₚ*→↪* t↪ₚ*t')))

ξₚ*-subst : ∀ {n} {t t' : Term (suc n)} {e₁ e₁' e₂ e₂' : Term n}
  → t ↪ₚ* t'
  → e₁ ↪ₚ* e₁'
  → e₂ ↪ₚ* e₂'
  -------------------------------
  → `subst t e₁ e₂ ↪ₚ* `subst t' e₁' e₂'
ξₚ*-subst t↪ₚ*t' e₁↪ₚ*e₁' e₂↪ₚ*e₂' = ↪*→↪ₚ* b
  where
    ξ-t = ξ*-subst₁ (↪ₚ*→↪* t↪ₚ*t')
    ξ-1 = ξ*-subst₂ (↪ₚ*→↪* e₁↪ₚ*e₁')
    ξ-2 = ξ*-subst₃ (↪ₚ*→↪* e₂↪ₚ*e₂')
    a = ↪*-trans ξ-t ξ-1
    b = ↪*-trans a ξ-2
--------------------------------------------------------------------------------
-- "Substituting two convertible terms into another term, yields again convertible terms."

-- A substitution σ₁ parallel-reduces in many steps to σ₂, if each
-- term of σ₁ parallel-reduces in many steps to the corresponding term of σ₂
_↪ₚ*σ_ : ∀ {m n} (σ₁ σ₂ : Sub m n) → Set
σ₁ ↪ₚ*σ σ₂ = ∀ x → σ₁ x ↪ₚ* σ₂ x

-- A substitution σ₁ reduces in many steps to σ₂, if each
-- term of σ₁ reduces in many steps to the corresponding term of σ₂
_↪*σ_ : ∀ {m n} (σ₁ σ₂ : Sub m n) → Set
σ₁ ↪*σ σ₂ = ∀ x → σ₁ x ↪* σ₂ x

-- A substitution σ₁ is convertible to a σ₂, if each
-- term of σ₁ is convertible to the corresponding term of σ₂
_≈σ_ : ∀ {m n} (σ₁ σ₂ : Sub m n) → Set
σ₁ ≈σ σ₂ = ∀ x → σ₁ x ≈ σ₂ x

↪ₚ*-ren :
  ∀ {m n} {t t' : Term m} (ρ : Ren m n) →
  t ↪ₚ* t' →
  ren ρ t ↪ₚ* ren ρ t'
↪ₚ*-ren ρ ↪ₚ*-refl = ↪ₚ*-refl
↪ₚ*-ren ρ (↪ₚ*-step t↪ₚt* t*↪ₚ*t') = ↪ₚ*-step (↪ₚ-ren ρ t↪ₚt*) (↪ₚ*-ren ρ t*↪ₚ*t')

↪ₚ*σ-ext :  ∀ {m n} {σ σ' : Sub m n}
  → σ ↪ₚ*σ σ'
  → extₛ σ ↪ₚ*σ extₛ σ'
↪ₚ*σ-ext σ↪σ' zero = ↪ₚ*-refl
↪ₚ*σ-ext σ↪σ' (suc x) = ↪ₚ*-ren wk (σ↪σ' x)

↪ₚ*σ-sub : ∀ {m n} {e : Term m} {σ σ' : Sub m n} →
  σ ↪ₚ*σ σ' →
  sub σ e ↪ₚ* sub σ' e
↪ₚ*σ-sub {m} {n} {`Set} {σ} {σ'} σ↪σ' = ↪ₚ*-refl
↪ₚ*σ-sub {m} {n} {`refl} {σ} {σ'} σ↪σ' = ↪ₚ*-refl
↪ₚ*σ-sub {m} {n} {` x} {σ} {σ'} σ↪σ' = σ↪σ' x
↪ₚ*σ-sub {m} {n} {`λ e} {σ} {σ'} σ↪σ' = ξₚ*-λ (↪ₚ*σ-sub {e = e} (↪ₚ*σ-ext σ↪σ'))
↪ₚ*σ-sub {m} {n} {l · r} {σ} {σ'} σ↪σ' = ξₚ*-· (↪ₚ*σ-sub {e = l} σ↪σ') (↪ₚ*σ-sub {e = r} σ↪σ')
↪ₚ*σ-sub {m} {n} {l `, r} {σ} {σ'} σ↪σ' = ξₚ*-, (↪ₚ*σ-sub {e = l} σ↪σ') (↪ₚ*σ-sub {e = r} σ↪σ')
↪ₚ*σ-sub {m} {n} {l `≡ r} {σ} {σ'} σ↪σ' = ξₚ*-≡ (↪ₚ*σ-sub {e = l} σ↪σ') (↪ₚ*σ-sub {e = r} σ↪σ')
↪ₚ*σ-sub {m} {n} {∀[x⦂ x ] e} {σ} {σ'} σ↪σ' = ξₚ*-∀ (↪ₚ*σ-sub {e = x} σ↪σ') (↪ₚ*σ-sub {e = e} (↪ₚ*σ-ext σ↪σ'))
↪ₚ*σ-sub {m} {n} {∃[x⦂ x ] e} {σ} {σ'} σ↪σ' = ξₚ*-∃ (↪ₚ*σ-sub {e = x} σ↪σ') (↪ₚ*σ-sub {e = e} (↪ₚ*σ-ext σ↪σ'))
↪ₚ*σ-sub {m} {n} {`proj₁ e} {σ} {σ'} σ↪σ' = ξₚ*-proj₁ (↪ₚ*σ-sub {e = e} (σ↪σ'))
↪ₚ*σ-sub {m} {n} {`proj₂ e} {σ} {σ'} σ↪σ' = ξₚ*-proj₂ (↪ₚ*σ-sub {e = e} (σ↪σ'))
↪ₚ*σ-sub {m} {n} {`subst t e₁ e₂} {σ} {σ'} σ↪σ' 
  = ξₚ*-subst (↪ₚ*σ-sub {e = t} (↪ₚ*σ-ext σ↪σ')) (↪ₚ*σ-sub {e = e₁} σ↪σ') (↪ₚ*σ-sub {e = e₂} σ↪σ')

↪*σ-sub : ∀ {m n} {e : Term m} {σ σ' : Sub m n} →
  σ ↪*σ σ' →
  sub σ e ↪* sub σ' e
↪*σ-sub {m} {n} {e} {σ} {σ'} σ↪σ' = ↪ₚ*→↪* (↪ₚ*σ-sub {m} {n} {e} {σ} {σ'} λ x → ↪*→↪ₚ* (σ↪σ' x))

ext-≈σ : ∀ {m n} {σ σ' : Sub m n}
  → σ ≈σ σ'
  → extₛ σ ≈σ extₛ σ'
ext-≈σ ≈ₛ zero = mk-≈ (` zero) ↪*-refl ↪*-refl
ext-≈σ ≈ₛ (suc x) with ≈ₛ x 
... | mk-≈ a σx↪*a σ'x↪*a = mk-≈ (ren suc a) (↪ₚ*→↪* (↪ₚ*-ren suc (↪*→↪ₚ* σx↪*a))) ((↪ₚ*→↪* (↪ₚ*-ren suc (↪*→↪ₚ* σ'x↪*a))))

≈σ-sub : ∀ {m n} {σ σ' : Sub m n} {e : Term m}
  → σ ≈σ σ'
  → sub σ e ≈ sub σ' e
≈σ-sub {e = ` x} ≈σ' = ≈σ' x
≈σ-sub {e = `Set} ≈σ' = ≈-refl
≈σ-sub {e = `refl} ≈σ' = ≈-refl
≈σ-sub {e = l · r} ≈σ' with ≈σ-sub {e = l} ≈σ' | ≈σ-sub {e = r} ≈σ'
... | mk-≈ l' σl↪*l' σ'l↪*l' | mk-≈ r' σr↪*r' σ'r↪*r' 
    = mk-≈ (l' · r') (↪*-trans (ξ*-·₁ σl↪*l') ((ξ*-·₂ σr↪*r'))) ((↪*-trans (ξ*-·₁ σ'l↪*l') ((ξ*-·₂ σ'r↪*r'))))
≈σ-sub {e = l `≡ r} ≈σ' with ≈σ-sub {e = l} ≈σ' | ≈σ-sub {e = r} ≈σ'
... | mk-≈ l' σl↪*l' σ'l↪*l' | mk-≈ r' σr↪*r' σ'r↪*r' 
    = mk-≈ (l' `≡ r') (↪*-trans (ξ*-≡₁ σl↪*l') ((ξ*-≡₂ σr↪*r'))) ((↪*-trans (ξ*-≡₁ σ'l↪*l') ((ξ*-≡₂ σ'r↪*r'))))
≈σ-sub {e = l `, r} ≈σ' with ≈σ-sub {e = l} ≈σ' | ≈σ-sub {e = r} ≈σ'
... | mk-≈ l' σl↪*l' σ'l↪*l' | mk-≈ r' σr↪*r' σ'r↪*r' 
    = mk-≈ (l' `, r') (↪*-trans (ξ*-,₁ σl↪*l') ((ξ*-,₂ σr↪*r'))) ((↪*-trans (ξ*-,₁ σ'l↪*l') ((ξ*-,₂ σ'r↪*r'))))
≈σ-sub {e = `λ e} ≈σ' with ≈σ-sub {e = e} (ext-≈σ ≈σ')
... | mk-≈ c eσx↪*a eσ'x↪*a = mk-≈ (`λ c) (ξ*-λ eσx↪*a) (ξ*-λ eσ'x↪*a)
≈σ-sub {e = `proj₁ e} ≈σ' with ≈σ-sub {e = e} ≈σ'
... | mk-≈ c eσx↪*a eσ'x↪*a = mk-≈ (`proj₁ c) (ξ*-proj₁ eσx↪*a) (ξ*-proj₁ eσ'x↪*a)
≈σ-sub {e = `proj₂ e} ≈σ' with ≈σ-sub {e = e} ≈σ'
... | mk-≈ c eσx↪*a eσ'x↪*a = mk-≈ (`proj₂ c) (ξ*-proj₂ eσx↪*a) (ξ*-proj₂ eσ'x↪*a)
≈σ-sub {e = ∀[x⦂ x ] e} ≈σ' with ≈σ-sub {e = x} ≈σ' | ≈σ-sub {e = e} (ext-≈σ ≈σ')
... | mk-≈ a x↪*a x'↪*a | mk-≈ b e↪*b e'↪*b 
    = mk-≈ (∀[x⦂ a ] b) (↪ₚ*→↪* (ξₚ*-∀ (↪*→↪ₚ* x↪*a) (↪*→↪ₚ* e↪*b))) (↪ₚ*→↪* (ξₚ*-∀ (↪*→↪ₚ* x'↪*a) (↪*→↪ₚ* e'↪*b)))
≈σ-sub {e = ∃[x⦂ x ] e} ≈σ' with ≈σ-sub {e = x} ≈σ' | ≈σ-sub {e = e} (ext-≈σ ≈σ')
... | mk-≈ a x↪*a x'↪*a | mk-≈ b e↪*b e'↪*b 
    = mk-≈ (∃[x⦂ a ] b) (↪ₚ*→↪* (ξₚ*-∃ (↪*→↪ₚ* x↪*a) (↪*→↪ₚ* e↪*b))) (↪ₚ*→↪* (ξₚ*-∃ (↪*→↪ₚ* x'↪*a) (↪*→↪ₚ* e'↪*b)))
≈σ-sub {e = `subst t e₁ e₂} ≈σ' with ≈σ-sub {e = t} (ext-≈σ ≈σ') | ≈σ-sub {e = e₁} ≈σ' | ≈σ-sub {e = e₂} ≈σ'
... | mk-≈ a t↪*a t'↪*a 
    | mk-≈ b e₁↪*b e₁'↪*b 
    | mk-≈ c e₂↪*c e₂'↪*c
 = mk-≈ (`subst a b c)  (↪ₚ*→↪* (ξₚ*-subst (↪*→↪ₚ* t↪*a) (↪*→↪ₚ* e₁↪*b) (↪*→↪ₚ* e₂↪*c))) 
                        (↪ₚ*→↪* (ξₚ*-subst (↪*→↪ₚ* t'↪*a) (↪*→↪ₚ* e₁'↪*b) (↪*→↪ₚ* e₂'↪*c)))

≈→≈σ : ∀ {n} {e e' : Term n}
  → e ≈ e'
  → 0↦ e ≈σ 0↦ e'
≈→≈σ e≈e' zero = e≈e'
≈→≈σ e≈e' (suc x) = mk-≈ (` x) ↪*-refl ↪*-refl

≈σ-sub₁ : ∀ {n} {e : Term (suc n)} {e₁ e₂ : Term n}
  → e₁ ≈ e₂
  → e [ e₁ ] ≈ e [ e₂ ]
≈σ-sub₁ {n} {e} {e₁} {e₂} e₁≈e₂ = ≈σ-sub {e = e} (≈→≈σ e₁≈e₂)

≈σ-refl : ∀ {m n} {σ : Sub m n} →
  σ ≈σ σ
≈σ-refl x = mk-≈ _ ↪*-refl ↪*-refl

--------------------------------------------------------------------------------
-- "Applying a substitution to two convertible terms, yields again convertible terms"

-- Renaming preserves reduction

      
β-λ₁ : ∀ {n} {e₁ : Term (suc n)} {e₂ : Term n}
      → (`λ e₁) · e₂ ↪ e₁ [ e₂ ] → Term (suc n)
β-λ₁ {e₁ = e₁} _ = e₁

β-λ₂ : ∀ {n} {e₁ : Term (suc n)} {e₂ : Term n}
      → (`λ e₁) · e₂ ↪ e₁ [ e₂ ] → Term n
β-λ₂ {e₂ = e₂} _ = e₂

↪-ren : ∀ {m n} {e e' : Term m} (ρ : Ren m n)
  → e ↪ e'
  → ren ρ e ↪ ren ρ e'
-- HINT: can also be solved with eq chains instead of subst
↪-ren ρ x@β-λ rewrite sym (swap-0↦-extᵣ-fusion ρ (β-λ₂ x) (β-λ₁ x)) = β-λ
↪-ren ρ (ξ-λ x) = ξ-λ (↪-ren (extᵣ ρ) x)
↪-ren ρ (ξ-proj₁ x) = ξ-proj₁ (↪-ren ρ x)
↪-ren ρ (ξ-proj₂ x) = ξ-proj₂ (↪-ren ρ x)
↪-ren ρ (ξ-·₁ x) = ξ-·₁ (↪-ren ρ x)
↪-ren ρ (ξ-·₂ x) = ξ-·₂ (↪-ren ρ x)
↪-ren ρ (ξ-≡₁ x) = ξ-≡₁ (↪-ren ρ x)
↪-ren ρ (ξ-≡₂ x) = ξ-≡₂ (↪-ren ρ x)
↪-ren ρ (ξ-,₁ x) = ξ-,₁ (↪-ren ρ x)
↪-ren ρ (ξ-,₂ x) = ξ-,₂ (↪-ren ρ x)
↪-ren ρ (ξ-∀₁ x) = ξ-∀₁ (↪-ren ρ x)
↪-ren ρ (ξ-∀₂ x) = ξ-∀₂ (↪-ren (extᵣ ρ) x)
↪-ren ρ β-proj₁ = β-proj₁
↪-ren ρ β-proj₂ = β-proj₂
↪-ren ρ β-subst = β-subst
↪-ren ρ (ξ-∃₁ x) = ξ-∃₁ (↪-ren ρ x)
↪-ren ρ (ξ-∃₂ x) = ξ-∃₂ (↪-ren (extᵣ ρ) x)
↪-ren ρ (ξ-subst₁ x) = ξ-subst₁ (↪-ren (extᵣ ρ) x)
↪-ren ρ (ξ-subst₂ x) = ξ-subst₂ (↪-ren ρ x)
↪-ren ρ (ξ-subst₃ x) = ξ-subst₃ (↪-ren ρ x)

-- Renaming preserves many reduction steps

↪*-ren : ∀ {m n} {e e' : Term m} (ρ : Ren m n)
  → e ↪* e'
  → ren ρ e ↪* ren ρ e'
↪*-ren ρ x = ↪ₚ*→↪* (↪ₚ*-ren ρ (↪*→↪ₚ* x))

-- Renaming preserves convertibility

≈-ren : ∀ {m n} {e e' : Term m} (ρ : Ren m n)
  → e ≈ e'
  → ren ρ e ≈ ren ρ e'
≈-ren ρ (mk-≈ c e↪*c e'↪*c) 
      =  mk-≈ (ren ρ c) (↪*-ren ρ e↪*c) (↪*-ren ρ e'↪*c)

-- Substitution preserves reduction

↪-sub : ∀ {m n} {e e' : Term m} (σ : Sub m n)
  → e ↪ e'
  → sub σ e ↪ sub σ e'
-- HINT: can also be solved with eq chains instead of subst
↪-sub σ x@β-λ rewrite sym (swap-0↦-extₛ-fusion σ (β-λ₂ x) (β-λ₁ x)) = β-λ
↪-sub σ (ξ-λ x) = ξ-λ (↪-sub (extₛ σ) x)
↪-sub σ (ξ-·₁ x) = ξ-·₁ (↪-sub σ x)
↪-sub σ (ξ-·₂ x) = ξ-·₂ (↪-sub σ x)
↪-sub σ (ξ-,₁ x) = ξ-,₁ (↪-sub σ x)
↪-sub σ (ξ-,₂ x) = ξ-,₂ (↪-sub σ x)
↪-sub σ (ξ-∀₁ x) = ξ-∀₁ (↪-sub σ x)
↪-sub σ (ξ-∀₂ x) = ξ-∀₂ (↪-sub (extₛ σ) x)
↪-sub σ (ξ-∃₁ x) = ξ-∃₁ (↪-sub σ x)
↪-sub σ (ξ-∃₂ x) = ξ-∃₂ (↪-sub (extₛ σ) x)
↪-sub σ β-proj₁ = β-proj₁
↪-sub σ β-proj₂ = β-proj₂
↪-sub σ β-subst = β-subst
↪-sub σ (ξ-proj₁ x) = ξ-proj₁ (↪-sub σ x)
↪-sub σ (ξ-proj₂ x) = ξ-proj₂ (↪-sub σ x)
↪-sub σ (ξ-≡₁ x) = ξ-≡₁ (↪-sub σ x)
↪-sub σ (ξ-≡₂ x) = ξ-≡₂ (↪-sub σ x)
↪-sub σ (ξ-subst₁ x) = ξ-subst₁ (↪-sub (extₛ σ) x)
↪-sub σ (ξ-subst₂ x) = ξ-subst₂ (↪-sub σ x)
↪-sub σ (ξ-subst₃ x) = ξ-subst₃ (↪-sub σ x)

-- Substitution preserves many reduction steps

↪*-sub : ∀ {m n} {e e' : Term m} (σ : Sub m n)
  → e ↪* e'
  → sub σ e ↪* sub σ e'
↪*-sub σ ↪*-refl = ↪*-refl
↪*-sub σ (↪*-step x x₁) = ↪*-step (↪-sub σ x) (↪*-sub σ x₁)

-- Substitution preserves convertibility

≈-sub : ∀ {m n} {e e' : Term m} (σ : Sub m n)
  → e ≈ e'
  → sub σ e ≈ sub σ e'
≈-sub σ (mk-≈ x e↪*x e'↪*x) 
      = mk-≈ (sub σ x) (↪*-sub σ e↪*x) (↪*-sub σ e'↪*x)

--------------------------------------------------------------------------------
-- "Typing is preserved along convertible types in the context"

-- Two contexts Γ₁ and Γ₂ are convertible, if each type in Γ₁ is
-- convertible to the corresponding type in Γ₂.

_≈ᶜ_ : ∀ {n} → Context n → Context n → Set
Γ₁ ≈ᶜ Γ₂ = ∀ x → lookup Γ₁ x ≈ lookup Γ₂ x

≈ᶜ-refl : ∀ {n} {Γ : Context n}
  → Γ ≈ᶜ Γ
≈ᶜ-refl x = ≈-refl

≈-ext : ∀ {n} {Γ₁ Γ₂ : Context n} {t₁ t₂ : Term n}
  → Γ₁ ≈ᶜ Γ₂
  → t₁ ≈ t₂
  → (Γ₁ , t₁) ≈ᶜ (Γ₂ , t₂)
≈-ext Γ₁≈Γ₂ t₁≈t₂ zero = ≈-ren wk t₁≈t₂
≈-ext Γ₁≈Γ₂ t₁≈t₂ (suc x) = ≈-ren wk (Γ₁≈Γ₂ x)

≈-Γ-⊢ : ∀ {n} {Γ₁ Γ₂ : Context n} {e t : Term n}
  → Γ₁ ≈ᶜ Γ₂
  → Γ₁ ⊢ e ⦂ t
  → Γ₂ ⊢ e ⦂ t
≈-Γ-⊢ Γ₁≈Γ₂ (⊢-` x refl) = ⊢-≈ (≈-sym (Γ₁≈Γ₂ x)) (⊢-` x refl)
≈-Γ-⊢ Γ₁≈Γ₂ (⊢-λ ⊢e₁ ⊢e₂) = ⊢-λ (≈-Γ-⊢ Γ₁≈Γ₂ ⊢e₁) (≈-Γ-⊢ (≈-ext Γ₁≈Γ₂ ≈-refl) ⊢e₂)
≈-Γ-⊢ Γ₁≈Γ₂ (⊢-· ⊢l ⊢r) = ⊢-· (≈-Γ-⊢ Γ₁≈Γ₂ ⊢l) (≈-Γ-⊢ Γ₁≈Γ₂ ⊢r)
≈-Γ-⊢ Γ₁≈Γ₂ (⊢-, ⊢l ⊢r) = ⊢-, (≈-Γ-⊢ Γ₁≈Γ₂ ⊢l) (≈-Γ-⊢ Γ₁≈Γ₂ ⊢r)
≈-Γ-⊢ Γ₁≈Γ₂ (⊢-≡ ⊢l ⊢r) = ⊢-≡ (≈-Γ-⊢ Γ₁≈Γ₂ ⊢l) (≈-Γ-⊢ Γ₁≈Γ₂ ⊢r)
≈-Γ-⊢ Γ₁≈Γ₂ (⊢-∀ ⊢e₁ ⊢e₂) = ⊢-∀ (≈-Γ-⊢ Γ₁≈Γ₂ ⊢e₁) (≈-Γ-⊢ (≈-ext Γ₁≈Γ₂ ≈-refl) ⊢e₂)
≈-Γ-⊢ Γ₁≈Γ₂ (⊢-∃ ⊢e₁ ⊢e₂) = ⊢-∃ (≈-Γ-⊢ Γ₁≈Γ₂ ⊢e₁) (≈-Γ-⊢ (≈-ext Γ₁≈Γ₂ ≈-refl) ⊢e₂)
≈-Γ-⊢ Γ₁≈Γ₂ ⊢-Set = ⊢-Set
≈-Γ-⊢ Γ₁≈Γ₂ (⊢-≈ x ⊢e) = ⊢-≈ x (≈-Γ-⊢ Γ₁≈Γ₂ ⊢e)
≈-Γ-⊢ Γ₁≈Γ₂ (⊢-proj₁ ⊢e) = ⊢-proj₁ (≈-Γ-⊢ Γ₁≈Γ₂ ⊢e)
≈-Γ-⊢ Γ₁≈Γ₂ (⊢-proj₂ ⊢e) = ⊢-proj₂ (≈-Γ-⊢ Γ₁≈Γ₂ ⊢e)
≈-Γ-⊢ Γ₁≈Γ₂ (⊢-refl  ⊢e) = ⊢-refl (≈-Γ-⊢ Γ₁≈Γ₂ ⊢e)
≈-Γ-⊢ Γ₁≈Γ₂ (⊢-subst t'⊢t ⊢u₁ ⊢u₂ ⊢≡ ⊢t[u₁]) 
  = ⊢-subst (≈-Γ-⊢ (≈-ext Γ₁≈Γ₂ ≈-refl) t'⊢t) (≈-Γ-⊢ Γ₁≈Γ₂ ⊢u₁) (≈-Γ-⊢ Γ₁≈Γ₂ ⊢u₂) (≈-Γ-⊢ Γ₁≈Γ₂ ⊢≡) (≈-Γ-⊢ Γ₁≈Γ₂ ⊢t[u₁])

≈-Γ-⊢₁ : ∀ {n} {Γ : Context n} {t₁ t₂ : Term n} {e t : Term (suc n)}
  → t₁ ≈ t₂
  → Γ , t₁ ⊢ e ⦂ t
  → Γ , t₂ ⊢ e ⦂ t
≈-Γ-⊢₁ t₁≈t₂ ⊢-Set = ⊢-Set
≈-Γ-⊢₁ t₁≈t₂ (⊢-refl e) = ⊢-refl (≈-Γ-⊢₁ t₁≈t₂ e)
≈-Γ-⊢₁ t₁≈t₂ (⊢-` x refl) = ⊢-≈ (≈-ext (λ _ → ≈-refl) (≈-sym t₁≈t₂) x) (⊢-` x refl )
≈-Γ-⊢₁ t₄≈t₂ (⊢-λ t₄⊢t₁ t₄,t₁⊢t₃) = ⊢-λ (≈-Γ-⊢₁ t₄≈t₂ t₄⊢t₁)   ((≈-Γ-⊢ (≈-ext (≈-ext (λ x → ≈-refl) t₄≈t₂) ≈-refl) t₄,t₁⊢t₃))
≈-Γ-⊢₁ t₁≈t₂ (⊢-proj₁ e) = ⊢-proj₁ (≈-Γ-⊢₁ t₁≈t₂ e)
≈-Γ-⊢₁ t₁≈t₂ (⊢-proj₂ e) = ⊢-proj₂ (≈-Γ-⊢₁ t₁≈t₂ e)
≈-Γ-⊢₁ t₁≈t₂ (⊢-· t⊢e t⊢e₁) = ⊢-· (≈-Γ-⊢₁ t₁≈t₂ t⊢e) (≈-Γ-⊢₁ t₁≈t₂ t⊢e₁)
≈-Γ-⊢₁ t₁≈t₂ (⊢-≡ t⊢e t⊢e₁) = ⊢-≡ (≈-Γ-⊢₁ t₁≈t₂ t⊢e) (≈-Γ-⊢₁ t₁≈t₂ t⊢e₁)
≈-Γ-⊢₁ t₁≈t₂ (⊢-, t⊢e t⊢e₁) = ⊢-, (≈-Γ-⊢₁ t₁≈t₂ t⊢e) (≈-Γ-⊢₁ t₁≈t₂ t⊢e₁)
≈-Γ-⊢₁ t₄≈t₂ (⊢-∀ t₄⊢t₁ t₄,t₁⊢t₃) = ⊢-∀ (≈-Γ-⊢₁ t₄≈t₂ t₄⊢t₁) (≈-Γ-⊢ (≈-ext (≈-ext (λ x → ≈-refl) t₄≈t₂) ≈-refl) t₄,t₁⊢t₃)
≈-Γ-⊢₁ t₄≈t₂ (⊢-∃ t₄⊢t₁ t₄,t₁⊢t₃) = ⊢-∃ (≈-Γ-⊢₁ t₄≈t₂ t₄⊢t₁) (≈-Γ-⊢ (≈-ext (≈-ext (λ x → ≈-refl) t₄≈t₂) ≈-refl) t₄,t₁⊢t₃)
≈-Γ-⊢₁ t₁≈t₂ (⊢-≈ x t⊢e) = ⊢-≈ x (≈-Γ-⊢₁ t₁≈t₂ t⊢e)
≈-Γ-⊢₁ t₁≈t₂ (⊢-subst t₁,t'⊢t t₁⊢u₁ t₁⊢u₂ t₁⊢≡ t₁⊢t[u₁]) 
  = ⊢-subst (≈-Γ-⊢ (≈-ext (≈-ext (λ x → ≈-refl) t₁≈t₂) ≈-refl) t₁,t'⊢t)
            (≈-Γ-⊢₁ t₁≈t₂ t₁⊢u₁)
            (≈-Γ-⊢₁ t₁≈t₂ t₁⊢u₂)
            (≈-Γ-⊢₁ t₁≈t₂ t₁⊢≡) 
            (≈-Γ-⊢₁ t₁≈t₂ t₁⊢t[u₁])