module univTypes.SubjectReduction.SubstitutionPreservesTyping 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.ConversionProperties using (≈-ren; ≈-sub)
open import univTypes.SubjectReduction.Composition using (wk-extᵣ-fusion; swap-0↦-extᵣ-fusion; wk-extₛ-fusion; swap-0↦-extₛ-fusion; wk-0↦-fusion)

open import univTypes.Util.Fin

-- Renaming Typings

infix 4 _⦂_⇒ᵣ_

_⦂_⇒ᵣ_ : ∀ {m n} → Ren m n → Context m → Context n → Set
ρ ⦂ Γ₁ ⇒ᵣ Γ₂ = ∀ x → lookup Γ₂ (ρ x) ≡ ren ρ (lookup Γ₁ x)

⊢extᵣ : ∀ {m n t ρ} {Γ₁ : Context m} {Γ₂ : Context n}
  → ρ      ⦂ Γ₁     ⇒ᵣ Γ₂ 
  → extᵣ ρ ⦂ Γ₁ , t ⇒ᵣ Γ₂ , (ren ρ t)
⊢extᵣ {ρ = ρ} ⊢ρ zero = wk-extᵣ-fusion _ _ 
⊢extᵣ ⊢ρ (suc x) rewrite ⊢ρ x = wk-extᵣ-fusion _ _
type : ∀ {n} {Γ : Context n} {e t : Term n} → Γ ⊢ e ⦂ t → Term n
type {t = t} _ = t

term : ∀ {n} {Γ : Context n} {e t : Term n} → Γ ⊢ e ⦂ t → Term n
term {e = e} _ = e

∀-type : ∀ {n} {Γ : Context n} {e : Term n}  {x t}
  → Γ ⊢ e ⦂ ∀[x⦂ x ] t
  → Term _
∀-type {t = t} _ = t

∃-type : ∀ {n} {Γ : Context n} {e : Term n}  {x t}
  → Γ ⊢ e ⦂ ∃[x⦂ x ] t
  → Term _
∃-type {t = t} _ = t

sub-type : ∀ {n} {Γ : Context n} {e : Term n}  {a b}
  → Γ ⊢ e ⦂ a [ b ] 
  → Term _
sub-type {a = a} _ = a

≡→≈ : ∀ {n} {a b : Term n} → a ≡ b → a ≈ b
≡→≈ refl = mk-≈ _ ↪*-refl ↪*-refl



⊢ren : ∀ {m n} {Γ₁ : Context m} {Γ₂ : Context n} {e t ρ}
  → ρ ⦂ Γ₁ ⇒ᵣ Γ₂ 
  → Γ₁ ⊢ e ⦂ t
  ------------------------
  → Γ₂ ⊢ ren ρ e ⦂ ren ρ t
⊢ren ⊢ρ ⊢-Set = ⊢-Set
⊢ren ⊢ρ (⊢-refl ⊢-e) = ⊢-refl (⊢ren ⊢ρ ⊢-e)
⊢ren ⊢ρ (⊢-` x refl) = ⊢-` _ (⊢ρ x)
⊢ren ⊢ρ (⊢-≡ ⊢l ⊢r) = ⊢-≡ (⊢ren ⊢ρ ⊢l) (⊢ren ⊢ρ ⊢r)
⊢ren {m} {n} {Γ₁} {Γ₂} {e} { ∃[x⦂ _ ] a } {ρ} ⊢ρ (⊢-, ⊢l ⊢r) 
  = ⊢-, (⊢ren ⊢ρ ⊢l) (⊢-≈ (≡→≈ (sym (swap-0↦-extᵣ-fusion ρ (term ⊢l) a) )) (⊢ren {Γ₂ = Γ₂} ⊢ρ ⊢r))
⊢ren ⊢ρ (⊢-≈ t₁≈t ⊢e) = ⊢-≈ (≈-ren _ t₁≈t) (⊢ren ⊢ρ ⊢e)
⊢ren ⊢ρ (⊢-∀ ⊢e₁ ⊢e₂) = ⊢-∀ (⊢ren ⊢ρ ⊢e₁) (⊢ren (⊢extᵣ ⊢ρ) ⊢e₂)
⊢ren ⊢ρ (⊢-∃ ⊢e₁ ⊢e₂) = ⊢-∃ (⊢ren ⊢ρ ⊢e₁) (⊢ren (⊢extᵣ ⊢ρ) ⊢e₂)
⊢ren ⊢ρ (⊢-λ ⊢t t⊢e) = ⊢-λ (⊢ren ⊢ρ ⊢t) (⊢ren (⊢extᵣ ⊢ρ) t⊢e)
⊢ren {ρ = ρ} ⊢ρ (⊢-· ⊢l ⊢r) = ⊢-≈ (≡→≈ ((swap-0↦-extᵣ-fusion ρ (term ⊢r) (∀-type ⊢l)))) (⊢-· (⊢ren ⊢ρ ⊢l)  (⊢ren ⊢ρ ⊢r))
⊢ren ⊢ρ (⊢-proj₁ ⊢e) = ⊢-proj₁ (⊢ren ⊢ρ ⊢e)
⊢ren {m} {n} {Γ₁} {Γ₂} {e} {t} {ρ} ⊢ρ (⊢-proj₂ ⊢e) 
  = ⊢-≈ (≡→≈ (swap-0↦-extᵣ-fusion ρ (`proj₁ (term ⊢e)) (∃-type ⊢e))) (⊢-proj₂ (⊢ren ⊢ρ ⊢e))
⊢ren {m} {n} {Γ₁} {Γ₂} {e} {t} {ρ} ⊢ρ x@(⊢-subst {t = t*} t'⊢t ⊢u₁ ⊢u₂ ⊢≡ ⊢t[u₁])
  = ⊢-≈ (≡→≈ (swap-0↦-extᵣ-fusion ρ (term ⊢u₂) t* ))
        (⊢-subst (⊢ren (⊢extᵣ ⊢ρ) t'⊢t) (⊢ren ⊢ρ ⊢u₁) (⊢ren ⊢ρ ⊢u₂) (⊢ren ⊢ρ ⊢≡) 
          (⊢-≈ (≡→≈ (sym (swap-0↦-extᵣ-fusion ρ (term ⊢u₁) (t*)))) (⊢ren ⊢ρ ⊢t[u₁])))
 
⊢wk : ∀ {n} {Γ : Context n} {t : Term n}
  → wk ⦂ Γ ⇒ᵣ (Γ , t)
⊢wk x = refl

-- Substitution Typings

infix 4 _⦂_⇒ₛ_

_⦂_⇒ₛ_ : ∀ {m n} → Sub m n → Context m → Context n → Set
σ ⦂ Γ₁ ⇒ₛ Γ₂ = ∀ x → Γ₂ ⊢ σ x ⦂ sub σ (lookup Γ₁ x)

⊢extₛ : ∀ {m n σ} {t : Term m} {Γ₁ : Context m} {Γ₂ : Context n}
  → σ      ⦂ Γ₁     ⇒ₛ Γ₂ 
  → extₛ σ ⦂ Γ₁ , t ⇒ₛ Γ₂ , (sub σ t)
⊢extₛ {σ = σ} {t = t} ⊢σ zero = ⊢-` zero (wk-extₛ-fusion σ t)
⊢extₛ {σ = σ} {Γ₁ = Γ₁} ⊢σ (suc x) = ⊢-≈ (≡→≈ (wk-extₛ-fusion σ (lookup Γ₁ x))) (⊢ren (λ _ → refl)  (⊢σ x))

⊢sub : ∀ {m n} {Γ₁ : Context m} {Γ₂ : Context n} {e t σ}
  → σ ⦂ Γ₁ ⇒ₛ Γ₂ 
  → Γ₁ ⊢ e ⦂ t
  ------------------------
  → Γ₂ ⊢ sub σ e ⦂ sub σ t
⊢sub ⊢σ ⊢-Set = ⊢-Set
⊢sub ⊢σ (⊢-` x refl) = ⊢σ x
⊢sub ⊢σ (⊢-refl e) = ⊢-refl (⊢sub ⊢σ e)
⊢sub {σ = σ} ⊢σ (⊢-· ⊢l ⊢r) = ⊢-≈ (≡→≈ (swap-0↦-extₛ-fusion σ (term ⊢r) (∀-type ⊢l))) (⊢-· (⊢sub ⊢σ ⊢l) (⊢sub ⊢σ ⊢r))
⊢sub ⊢σ (⊢-≡ ⊢l ⊢r) = ⊢-≡ (⊢sub ⊢σ ⊢l) (⊢sub ⊢σ ⊢r)
⊢sub {σ = σ} ⊢σ (⊢-, {e₁ = e₁} {t₂ = t₂} ⊢l ⊢r) 
  = ⊢-, (⊢sub ⊢σ ⊢l) (⊢-≈ (≡→≈ (sym (swap-0↦-extₛ-fusion σ e₁ t₂))) (⊢sub ⊢σ ⊢r))
⊢sub {σ = σ} ⊢σ (⊢-≈ t'≈t ⊢e) = ⊢-≈ (≈-sub σ t'≈t) (⊢sub ⊢σ ⊢e)
⊢sub ⊢σ (⊢-λ ⊢e₁ ⊢e₂) = ⊢-λ (⊢sub ⊢σ ⊢e₁) (⊢sub (⊢extₛ ⊢σ) ⊢e₂)
⊢sub ⊢σ (⊢-∀ ⊢e₁ ⊢e₂) = ⊢-∀ (⊢sub ⊢σ ⊢e₁) (⊢sub (⊢extₛ ⊢σ) ⊢e₂)
⊢sub ⊢σ (⊢-∃ ⊢e₁ ⊢e₂) = ⊢-∃ (⊢sub ⊢σ ⊢e₁) (⊢sub (⊢extₛ ⊢σ) ⊢e₂)
⊢sub ⊢σ (⊢-proj₁ e) = ⊢-proj₁ (⊢sub ⊢σ e)
⊢sub {m} {n} {Γ₁} {Γ₂} {e} {t} {σ} ⊢σ (⊢-proj₂ {e = a} {t₂ = t₂} ⊢e) 
  = ⊢-≈ (≡→≈ (swap-0↦-extₛ-fusion σ (`proj₁ a) t₂)) (⊢-proj₂ (⊢sub ⊢σ ⊢e))
⊢sub {m} {n} {Γ₁} {Γ₂} {e} {t} {σ} ⊢σ (⊢-subst {t = t*} t'⊢t ⊢u₁ ⊢u₂ ⊢≡ ⊢t[u₁])
  = ⊢-≈ (≡→≈ (swap-0↦-extₛ-fusion σ (term ⊢u₂) t* ))
        (⊢-subst (⊢sub (⊢extₛ ⊢σ) t'⊢t) (⊢sub ⊢σ ⊢u₁) (⊢sub ⊢σ ⊢u₂) (⊢sub ⊢σ ⊢≡) 
          (⊢-≈ (≡→≈ (sym (swap-0↦-extₛ-fusion σ (term ⊢u₁) (t*)))) (⊢sub ⊢σ ⊢t[u₁])))

⊢sub₁ : ∀ {n} {Γ : Context n} {e : Term n} {t}
  → Γ ⊢ e ⦂ t
  → 0↦ e ⦂ Γ , t ⇒ₛ Γ
⊢sub₁ {n} {Γ} {e} {t} ⊢e zero = ⊢-≈ (≡→≈ (sym (wk-0↦-fusion e t)))  ⊢e
⊢sub₁ {n} {Γ} {e} {t} ⊢e (suc x) = ⊢-` x (sym (wk-0↦-fusion e (lookup Γ x) ))