126 lines
6.6 KiB
Agda
126 lines
6.6 KiB
Agda
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) ))
|