From e8ee5b200c56c5b164729f6da22e49e5db6b84bd Mon Sep 17 00:00:00 2001 From: JKF Date: Sat, 25 Apr 2026 21:57:10 +0200 Subject: [PATCH] Some definitions and adjusted proofs --- SubjectReduction/ConversionProperties.agda | 95 ++++++++++++------- SubjectReduction/Inversion.agda | 21 ++-- SubjectReduction/SubjectReduction.agda | 29 ++---- .../SubstitutionPreservesTyping.agda | 17 +++- 4 files changed, 96 insertions(+), 66 deletions(-) diff --git a/SubjectReduction/ConversionProperties.agda b/SubjectReduction/ConversionProperties.agda index 083fcf6..07d7888 100644 --- a/SubjectReduction/ConversionProperties.agda +++ b/SubjectReduction/ConversionProperties.agda @@ -11,7 +11,7 @@ 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 (ξ*-∃₁; ξ*-∃₂; ξ*-,₁; ξ*-,₂; ξ*-≡₁; ξ*-≡₂; ξ*-proj₁; ξ*-proj₂; ξ*-Setn; ξ*-Setω; ξ*-lsuc; ξ*-⊔₁; ξ*-⊔₂) 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 @@ -126,13 +126,35 @@ open import univTypes.Util.Fin a = ↪*-trans ξ-t ξ-1 b = ↪*-trans a ξ-2 - -- New ξₚ*-Setn : ∀ {n} {e e' : Term n} → e ↪ₚ* e' --------------- → `Setn e ↪ₚ* `Setn e' -ξₚ*-Setn e↪ₚ*e' = {! ↪*→↪ₚ* ? !} +ξₚ*-Setn e↪ₚ*e' = ↪*→↪ₚ* (ξ*-Setn (↪ₚ*→↪* e↪ₚ*e')) + +ξₚ*-Setω : ∀ {n} {e e' : Term n} + → e ↪ₚ* e' + --------------- + → `Setω e ↪ₚ* `Setω e' +ξₚ*-Setω e↪ₚ*e' = ↪*→↪ₚ* (ξ*-Setω (↪ₚ*→↪* e↪ₚ*e')) + + +ξₚ*-lsuc : ∀ {n} {e e' : Term n} + → e ↪ₚ* e' + --------------- + → `lsuc e ↪ₚ* `lsuc e' +ξₚ*-lsuc e↪ₚ*e' = ↪*→↪ₚ* (ξ*-lsuc (↪ₚ*→↪* 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₂'))) + -- ↪*→↪ₚ* (ξ*-Setn (↪ₚ*→↪* e↪ₚ*e')) -------------------------------------------------------------------------------- -- "Substituting two convertible terms into another term, yields again convertible terms." @@ -182,10 +204,10 @@ _≈σ_ : ∀ {m n} (σ₁ σ₂ : Sub m n) → Set = ξₚ*-subst (↪ₚ*σ-sub {e = t} (↪ₚ*σ-ext σ↪σ')) (↪ₚ*σ-sub {e = e₁} σ↪σ') (↪ₚ*σ-sub {e = e₂} σ↪σ') ↪ₚ*σ-sub {m} {n} {`Level} {σ} {σ'} σ↪σ' = ↪ₚ*-refl ↪ₚ*σ-sub {m} {n} {`lzero} {σ} {σ'} σ↪σ' = ↪ₚ*-refl -↪ₚ*σ-sub {m} {n} {`Setω x} {σ} {σ'} σ↪σ' = {! ξₚ*-Setω (↪ₚ*σ-sub {e = e} (σ↪σ') !} -↪ₚ*σ-sub {m} {n} {`Setn x} {σ} {σ'} σ↪σ' = {! !} -↪ₚ*σ-sub {m} {n} {`lsuc x} {σ} {σ'} σ↪σ' = {! !} -↪ₚ*σ-sub {m} {n} {l `⊔ r} {σ} {σ'} σ↪σ' = {! ξₚ*-⊔ (↪ₚ*σ-sub {e = l} σ↪σ') (↪ₚ*σ-sub {e = r} σ↪σ') !} +↪ₚ*σ-sub {m} {n} {`Setω e} {σ} {σ'} σ↪σ' = ξₚ*-Setω (↪ₚ*σ-sub {e = e} σ↪σ') +↪ₚ*σ-sub {m} {n} {`Setn e} {σ} {σ'} σ↪σ' = ξₚ*-Setn (↪ₚ*σ-sub {e = e} σ↪σ') +↪ₚ*σ-sub {m} {n} {`lsuc e} {σ} {σ'} σ↪σ' = ξₚ*-lsuc (↪ₚ*σ-sub {e = e} σ↪σ') +↪ₚ*σ-sub {m} {n} {l `⊔ r} {σ} {σ'} σ↪σ' = ξₚ*-⊔ (↪ₚ*σ-sub {e = l} σ↪σ') (↪ₚ*σ-sub {e = r} σ↪σ') ↪*σ-sub : ∀ {m n} {e : Term m} {σ σ' : Sub m n} → σ ↪*σ σ' → @@ -231,8 +253,17 @@ ext-≈σ ≈ₛ (suc x) with ≈ₛ x | 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))) -≈σ-sub {zero} ≈σ' = {! !} -≈σ-sub {suc e} ≈σ' = {! !} +≈σ-sub {e = `Level} ≈σ' = mk-≈ `Level ↪*-refl ↪*-refl +≈σ-sub {e = `lzero} ≈σ' = mk-≈ `lzero ↪*-refl ↪*-refl +≈σ-sub {e = `Setω e} ≈σ' with ≈σ-sub {e = e} ≈σ' +... | mk-≈ e' e↪*e' e₁↪*e' = mk-≈ (`Setω e') (ξ*-Setω e↪*e') (ξ*-Setω e₁↪*e') +≈σ-sub {e = `Setn e} ≈σ' with ≈σ-sub {e = e} ≈σ' +... | mk-≈ e' e↪*e' e₁↪*e' = mk-≈ (`Setn e') (ξ*-Setn e↪*e') (ξ*-Setn e₁↪*e') +≈σ-sub {e = `lsuc e} ≈σ' with ≈σ-sub {e = e} ≈σ' +... | mk-≈ e' e↪*e' e₁↪*e' = mk-≈ (`lsuc e') (ξ*-lsuc e↪*e') (ξ*-lsuc e₁↪*e') +≈σ-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'))) ≈→≈σ : ∀ {n} {e e' : Term n} → e ≈ e' @@ -288,11 +319,11 @@ ext-≈σ ≈ₛ (suc x) with ≈ₛ x ↪-ren ρ (ξ-subst₂ x) = ξ-subst₂ (↪-ren ρ x) ↪-ren ρ (ξ-subst₃ x) = ξ-subst₃ (↪-ren ρ x) -- New -↪-ren ρ (ξ-⊔₁ x) = {! !} -↪-ren ρ (ξ-⊔₂ x) = {! !} -↪-ren ρ (ξ-lsuc x) = {! !} -↪-ren ρ (ξ-Setn x) = {! !} -↪-ren ρ (ξ-Setω x) = {! !} +↪-ren ρ (ξ-⊔₁ x) = ξ-⊔₁ (↪-ren ρ x) +↪-ren ρ (ξ-⊔₂ x) = ξ-⊔₂ (↪-ren ρ x) +↪-ren ρ (ξ-lsuc x) = ξ-lsuc (↪-ren ρ x) +↪-ren ρ (ξ-Setn x) = ξ-Setn (↪-ren ρ x) +↪-ren ρ (ξ-Setω x) = ξ-Setω (↪-ren ρ x) -- Renaming preserves many reduction steps @@ -335,12 +366,12 @@ ext-≈σ ≈ₛ (suc x) with ≈ₛ x ↪-sub σ (ξ-subst₁ x) = ξ-subst₁ (↪-sub (extₛ σ) x) ↪-sub σ (ξ-subst₂ x) = ξ-subst₂ (↪-sub σ x) -- New -↪-sub σ (ξ-⊔₁ x) = {! !} -↪-sub σ (ξ-⊔₂ x) = {! !} -↪-sub σ (ξ-lsuc x) = {! !} -↪-sub σ (ξ-Setn x) = {! !} -↪-sub σ (ξ-subst₃ x) = {! !} -↪-sub σ (ξ-Setω x) = {! !} +↪-sub σ (ξ-⊔₁ x) = ξ-⊔₁ (↪-sub σ x) +↪-sub σ (ξ-⊔₂ x) = ξ-⊔₂ (↪-sub σ x) +↪-sub σ (ξ-lsuc x) = ξ-lsuc (↪-sub σ x) +↪-sub σ (ξ-Setn x) = ξ-Setn (↪-sub σ x) +↪-sub σ (ξ-subst₃ x) = ξ-subst₃ (↪-sub σ x) +↪-sub σ (ξ-Setω x) = ξ-Setω (↪-sub σ x) -- Substitution preserves many reduction steps @@ -396,12 +427,12 @@ _≈ᶜ_ : ∀ {n} → Context n → Context n → Set ≈-Γ-⊢ Γ₁≈Γ₂ (⊢-subst t'⊢t ⊢u₁ ⊢u₂ ⊢≡ ⊢t[u₁]) = ⊢-subst (≈-Γ-⊢ (≈-ext Γ₁≈Γ₂ ≈-refl) t'⊢t) (≈-Γ-⊢ Γ₁≈Γ₂ ⊢u₁) (≈-Γ-⊢ Γ₁≈Γ₂ ⊢u₂) (≈-Γ-⊢ Γ₁≈Γ₂ ⊢≡) (≈-Γ-⊢ Γ₁≈Γ₂ ⊢t[u₁]) -- New -≈-Γ-⊢ Γ₁≈Γ₂ ⊢-Setn = {! !} -≈-Γ-⊢ Γ₁≈Γ₂ ⊢-Setω = {! !} -≈-Γ-⊢ Γ₁≈Γ₂ ⊢-lzero = {! !} -≈-Γ-⊢ Γ₁≈Γ₂ (⊢-lsuc ⊢x) = {! !} -≈-Γ-⊢ Γ₁≈Γ₂ (⊢-⊔ ⊢x ⊢x₁) = {! !} -≈-Γ-⊢ Γ₁≈Γ₂ ⊢-Level = {! !} +≈-Γ-⊢ Γ₁≈Γ₂ ⊢-Setn = ⊢-Setn +≈-Γ-⊢ Γ₁≈Γ₂ ⊢-Setω = ⊢-Setω +≈-Γ-⊢ Γ₁≈Γ₂ ⊢-lzero = ⊢-lzero +≈-Γ-⊢ Γ₁≈Γ₂ (⊢-lsuc ⊢x) = ⊢-lsuc (≈-Γ-⊢ Γ₁≈Γ₂ ⊢x) +≈-Γ-⊢ Γ₁≈Γ₂ (⊢-⊔ ⊢x ⊢x₁) = ⊢-⊔ (≈-Γ-⊢ Γ₁≈Γ₂ ⊢x) (≈-Γ-⊢ Γ₁≈Γ₂ ⊢x₁) +≈-Γ-⊢ Γ₁≈Γ₂ ⊢-Level = ⊢-Level ≈-Γ-⊢₁ : ∀ {n} {Γ : Context n} {t₁ t₂ : Term n} {e t : Term (suc n)} → t₁ ≈ t₂ @@ -424,9 +455,9 @@ _≈ᶜ_ : ∀ {n} → Context n → Context n → Set (≈-Γ-⊢₁ t₁≈t₂ t₁⊢u₂) (≈-Γ-⊢₁ t₁≈t₂ t₁⊢≡) (≈-Γ-⊢₁ t₁≈t₂ t₁⊢t[u₁]) -≈-Γ-⊢₁ t₁≈t₂ ⊢-Setn = {! !} -≈-Γ-⊢₁ t₁≈t₂ ⊢-Setω = {! !} -≈-Γ-⊢₁ t₁≈t₂ ⊢-lzero = {! !} -≈-Γ-⊢₁ t₁≈t₂ (⊢-lsuc ⊢x) = {! !} -≈-Γ-⊢₁ t₁≈t₂ (⊢-⊔ ⊢x ⊢x₁) = {! !} -≈-Γ-⊢₁ t₁≈t₂ ⊢-Level = {! !} +≈-Γ-⊢₁ t₁≈t₂ ⊢-Setn = ⊢-Setn +≈-Γ-⊢₁ t₁≈t₂ ⊢-Setω = ⊢-Setω +≈-Γ-⊢₁ t₁≈t₂ ⊢-lzero = ⊢-lzero +≈-Γ-⊢₁ t₁≈t₂ (⊢-lsuc ⊢x) = ⊢-lsuc (≈-Γ-⊢₁ t₁≈t₂ ⊢x) +≈-Γ-⊢₁ t₁≈t₂ (⊢-⊔ ⊢x ⊢x₁) = ⊢-⊔ (≈-Γ-⊢₁ t₁≈t₂ ⊢x) (≈-Γ-⊢₁ t₁≈t₂ ⊢x₁) +≈-Γ-⊢₁ t₁≈t₂ ⊢-Level = ⊢-Level diff --git a/SubjectReduction/Inversion.agda b/SubjectReduction/Inversion.agda index 5ba2808..2ae9d87 100644 --- a/SubjectReduction/Inversion.agda +++ b/SubjectReduction/Inversion.agda @@ -41,27 +41,28 @@ invert-≈-∀ (mk-≈ x ∀₁↪*x ∀₂↪*x) with ↪*-∀-shape ∀₁↪* invert-⊢λ' : ∀ {n} {Γ : Context n} {e : Term (suc n)} {t : Term n} → Γ ⊢ `λ e ⦂ t → - ∃[ t₁ ] ∃[ t₂ ] + ∃[ t₁ ] ∃[ t₂ ] ∃[ l ] t ≈ (∀[x⦂ t₁ ] t₂) × - Γ ⊢ t₁ ⦂ `Set × + Γ ⊢ t₁ ⦂ (`Setn l) × Γ , t₁ ⊢ e ⦂ t₂ -invert-⊢λ' (⊢-λ ⊢λ ⊢e) = ⟨ _ , ⟨ _ , ⟨ ≈-refl , ⟨ ⊢λ , ⊢e ⟩ ⟩ ⟩ ⟩ +invert-⊢λ' (⊢-λ ⊢λ ⊢e) = ⟨ _ , ⟨ _ , ⟨ _ , ⟨ ≈-refl , ⟨ ⊢λ , ⊢e ⟩ ⟩ ⟩ ⟩ ⟩ invert-⊢λ' (⊢-≈ t₁≈t ⊢λ⦂t₁) with invert-⊢λ' ⊢λ⦂t₁ -... | ⟨ X , ⟨ E , ⟨ t₁≈∀[X]E , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩ - = ⟨ X , ⟨ E , ⟨ ≈-trans (≈-sym t₁≈t) t₁≈∀[X]E , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩ +... | ⟨ X , ⟨ E , ⟨ L , ⟨ t₁≈∀[X]E , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩ ⟩ + = ⟨ X , ⟨ E , ⟨ _ , ⟨ ≈-trans (≈-sym t₁≈t) t₁≈∀[X]E , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩ ⟩ invert-⊢λ : ∀ {n} {Γ : Context n} {e : Term (suc n)} {t₁ : Term n} {t₂ : Term (suc n)} → Γ ⊢ `λ e ⦂ ∀[x⦂ t₁ ] t₂ - → ∃[ t₁' ] ∃[ t₂' ] + → ∃[ t₁' ] ∃[ t₂' ] ∃[ l ] t₁ ≈ t₁' × t₂ ≈ t₂' × - Γ ⊢ t₁' ⦂ `Set × + Γ ⊢ t₁' ⦂ (`Setn l) × Γ , t₁' ⊢ e ⦂ t₂' -invert-⊢λ (⊢-λ ⊢λ ⊢λ₁) = ⟨ _ , ⟨ _ , ⟨ mk-≈ _ ↪*-refl ↪*-refl , ⟨ mk-≈ _ ↪*-refl ↪*-refl , ⟨ ⊢λ , ⊢λ₁ ⟩ ⟩ ⟩ ⟩ ⟩ +invert-⊢λ (⊢-λ ⊢λ ⊢λ₁) = ⟨ _ , ⟨ _ , ⟨ _ , ⟨ mk-≈ _ ↪*-refl ↪*-refl , ⟨ mk-≈ _ ↪*-refl ↪*-refl , ⟨ ⊢λ , ⊢λ₁ ⟩ ⟩ ⟩ ⟩ ⟩ ⟩ invert-⊢λ (⊢-≈ t≈∀ ⊢λ) with invert-⊢λ' ⊢λ -... | ⟨ X , ⟨ E , ⟨ t≈∀' , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩ with invert-≈-∀ (≈-trans (≈-sym t≈∀) t≈∀') +... | ⟨ X , ⟨ E , ⟨ L , ⟨ t≈∀' , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩ ⟩ with invert-≈-∀ (≈-trans (≈-sym t≈∀) t≈∀') ... | ⟨ ≈₁ , ≈₂ ⟩ - = ⟨ X , ⟨ E , ⟨ ≈₁ , ⟨ ≈₂ , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩ ⟩ + = ⟨ X , ⟨ E , ⟨ L , ⟨ ≈₁ , ⟨ ≈₂ , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩ ⟩ ⟩ + -- Inversion for pairs diff --git a/SubjectReduction/SubjectReduction.agda b/SubjectReduction/SubjectReduction.agda index 14c6a68..78adfb5 100644 --- a/SubjectReduction/SubjectReduction.agda +++ b/SubjectReduction/SubjectReduction.agda @@ -27,12 +27,7 @@ subject-reduction : ∀ {n} {Γ : Context n} {e e' t : Term n} → e ↪ e' ---------- → Γ ⊢ e' ⦂ t -subject-reduction (⊢-≈ t≈t₁ ⊢e) β-λ = ⊢-≈ t≈t₁ (subject-reduction ⊢e β-λ) -subject-reduction (⊢-≈ t≈t₁ ⊢e) (ξ-λ e↪e') = ⊢-≈ t≈t₁ (subject-reduction ⊢e (ξ-λ e↪e')) -subject-reduction (⊢-≈ t≈t₁ ⊢e) (ξ-·₁ e↪e') = ⊢-≈ t≈t₁ (subject-reduction ⊢e (ξ-·₁ e↪e')) -subject-reduction (⊢-≈ t≈t₁ ⊢e) (ξ-·₂ e↪e') = ⊢-≈ t≈t₁ (subject-reduction ⊢e (ξ-·₂ e↪e')) -subject-reduction (⊢-≈ t≈t₁ ⊢e) (ξ-∀₁ e↪e') = ⊢-≈ t≈t₁ (subject-reduction ⊢e (ξ-∀₁ e↪e')) -subject-reduction (⊢-≈ t≈t₁ ⊢e) (ξ-∀₂ e↪e') = ⊢-≈ t≈t₁ (subject-reduction ⊢e (ξ-∀₂ e↪e')) +subject-reduction (⊢-≈ t≈t ⊢e) e↪e' = ⊢-≈ t≈t (subject-reduction ⊢e e↪e') subject-reduction (⊢-λ ⊢e₁ ⊢e₂) (ξ-λ e₁↪e₁') = ⊢-λ ⊢e₁ (subject-reduction ⊢e₂ e₁↪e₁') subject-reduction (⊢-· ⊢e₁ ⊢e₂) (ξ-·₁ e₁↪e₁') = ⊢-· (subject-reduction ⊢e₁ e₁↪e₁') ⊢e₂ subject-reduction (⊢-· ⊢e₁ ⊢e₂) (ξ-·₂ e₂↪e₂') = @@ -41,26 +36,11 @@ subject-reduction (⊢-∀ ⊢t ⊢e) (ξ-∀₁ t↪t') = ⊢-∀ (subject-reduction ⊢t t↪t') (≈-Γ-⊢₁ (↪→≈ t↪t') ⊢e) subject-reduction (⊢-∀ ⊢e₁ ⊢e₂) (ξ-∀₂ e₁↪e₁') = ⊢-∀ ⊢e₁ (subject-reduction ⊢e₂ e₁↪e₁') subject-reduction (⊢-· ⊢e₁ ⊢e₂) β-λ with invert-⊢λ ⊢e₁ -... | ⟨ t₁' , ⟨ t₂' , ⟨ t₁≈t₁' , ⟨ t₂≈t₂' , ⟨ ⊢t₁' , Γ,t₁'⊢e₁⦂t₂' ⟩ ⟩ ⟩ ⟩ ⟩ +... | ⟨ t₁' , ⟨ t₂' , ⟨ lvl , ⟨ t₁≈t₁' , ⟨ t₂≈t₂' , ⟨ ⊢t₁' , Γ,t₁'⊢e₁⦂t₂' ⟩ ⟩ ⟩ ⟩ ⟩ ⟩ = ⊢sub (⊢sub₁ (⊢-≈ t₁≈t₁' ⊢e₂)) ⊢e₁⦂t₂ where ⊢e₁⦂t₂ = ⊢-≈ (≈-sym t₂≈t₂') Γ,t₁'⊢e₁⦂t₂' subject-reduction (⊢-` x x₁) () -subject-reduction ⊢-Set () -subject-reduction (⊢-≈ x ⊢e) β-proj₁ = ⊢-≈ x (subject-reduction ⊢e β-proj₁) -subject-reduction (⊢-≈ x ⊢e) β-proj₂ = ⊢-≈ x (subject-reduction ⊢e β-proj₂) -subject-reduction (⊢-≈ x ⊢e) β-subst = ⊢-≈ x (subject-reduction ⊢e β-subst) -subject-reduction (⊢-≈ x ⊢e) (ξ-∃₁ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-∃₁ e↪e')) -subject-reduction (⊢-≈ x ⊢e) (ξ-∃₂ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-∃₂ e↪e')) -subject-reduction (⊢-≈ x ⊢e) (ξ-proj₁ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-proj₁ e↪e')) -subject-reduction (⊢-≈ x ⊢e) (ξ-proj₂ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-proj₂ e↪e')) -subject-reduction (⊢-≈ x ⊢e) (ξ-,₁ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-,₁ e↪e')) -subject-reduction (⊢-≈ x ⊢e) (ξ-,₂ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-,₂ e↪e')) -subject-reduction (⊢-≈ x ⊢e) (ξ-≡₁ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-≡₁ e↪e')) -subject-reduction (⊢-≈ x ⊢e) (ξ-≡₂ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-≡₂ e↪e')) -subject-reduction (⊢-≈ t₁≈t ⊢e) (ξ-subst₁ t₂↪t') = ⊢-≈ t₁≈t (subject-reduction ⊢e (ξ-subst₁ t₂↪t')) -subject-reduction (⊢-≈ x ⊢e) (ξ-subst₂ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-subst₂ e↪e')) -subject-reduction (⊢-≈ x ⊢e) (ξ-subst₃ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-subst₃ e↪e')) subject-reduction (⊢-∃ ⊢t₁ t₁⊢t₂) (ξ-∃₁ t₁↪t₁') = ⊢-∃ (subject-reduction ⊢t₁ t₁↪t₁') (≈-Γ-⊢₁ (↪→≈ t₁↪t₁') t₁⊢t₂) subject-reduction (⊢-∃ ⊢e ⊢e₁) (ξ-∃₂ e↪e') = ⊢-∃ ⊢e (subject-reduction ⊢e₁ e↪e') @@ -88,3 +68,8 @@ subject-reduction (⊢-subst {u₁ = u₁} {u₂ = u₂} ⊢t ⊢u₁ ⊢u₂ = ⊢-≈ (≈-sym (≈-sub (0↦ u₂) (↪→≈ t↪t'))) (⊢-subst (subject-reduction ⊢t t↪t') ⊢u₁ ⊢u₂ ⊢≈ (⊢-≈ (≈-sub (0↦ u₁) (↪→≈ t↪t')) ⊢t[u₁])) subject-reduction (⊢-subst ⊢e ⊢e₁ ⊢e₂ ⊢e₃ ⊢e₄) (ξ-subst₂ e↪e') = ⊢-subst ⊢e ⊢e₁ ⊢e₂ (subject-reduction ⊢e₃ e↪e') ⊢e₄ subject-reduction (⊢-subst ⊢e ⊢e₁ ⊢e₂ ⊢e₃ ⊢e₄) (ξ-subst₃ e↪e') = ⊢-subst ⊢e ⊢e₁ ⊢e₂ ⊢e₃ (subject-reduction ⊢e₄ e↪e') +subject-reduction (⊢-lsuc a) (ξ-lsuc l↪l') = ⊢-lsuc (subject-reduction a l↪l') +subject-reduction (⊢-⊔ a a₁) (ξ-⊔₁ l↪l') = ⊢-⊔ (subject-reduction a l↪l') a₁ +subject-reduction (⊢-⊔ a a₁) (ξ-⊔₂ l↪l') = ⊢-⊔ a (subject-reduction a₁ l↪l') +subject-reduction ⊢-Setn (ξ-Setn l↪l') = ⊢-≈ (mk-≈ (`Setn `lsuc _) ↪*-refl (↪*-step (ξ-Setn (ξ-lsuc l↪l')) ↪*-refl) ) ⊢-Setn +subject-reduction ⊢-Setω (ξ-Setω l↪l') = ⊢-≈ (mk-≈ (`Setω `lsuc _) ↪*-refl (↪*-step (ξ-Setω (ξ-lsuc l↪l')) ↪*-refl) ) ⊢-Setω diff --git a/SubjectReduction/SubstitutionPreservesTyping.agda b/SubjectReduction/SubstitutionPreservesTyping.agda index b088f49..82fd1c4 100644 --- a/SubjectReduction/SubstitutionPreservesTyping.agda +++ b/SubjectReduction/SubstitutionPreservesTyping.agda @@ -58,7 +58,6 @@ sub-type {a = a} _ = a → Γ₁ ⊢ 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) @@ -76,6 +75,14 @@ sub-type {a = a} _ = a = ⊢-≈ (≡→≈ (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₁]))) +-- New +⊢ren ⊢ρ ⊢-Setn = ⊢-Setn +⊢ren ⊢ρ ⊢-Setω = ⊢-Setω +⊢ren ⊢ρ ⊢-lzero = ⊢-lzero +⊢ren ⊢ρ (⊢-lsuc ⊢e) = ⊢-lsuc (⊢ren ⊢ρ ⊢e) +⊢ren ⊢ρ (⊢-⊔ ⊢l ⊢r) = ⊢-⊔ (⊢ren ⊢ρ ⊢l) (⊢ren ⊢ρ ⊢r) +⊢ren ⊢ρ ⊢-Level = ⊢-Level + ⊢wk : ∀ {n} {Γ : Context n} {t : Term n} → wk ⦂ Γ ⇒ᵣ (Γ , t) @@ -99,7 +106,6 @@ _⦂_⇒ₛ_ : ∀ {m n} → Sub m n → Context m → Context n → Set → Γ₁ ⊢ 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)) @@ -117,6 +123,13 @@ _⦂_⇒ₛ_ : ∀ {m n} → Sub m n → Context m → Context n → Set = ⊢-≈ (≡→≈ (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₁]))) +-- New +⊢sub ⊢σ ⊢-Setn = ⊢-Setn +⊢sub ⊢σ ⊢-Setω = ⊢-Setω +⊢sub ⊢σ ⊢-lzero = ⊢-lzero +⊢sub ⊢σ ⊢-Level = ⊢-Level +⊢sub ⊢σ (⊢-lsuc ⊢e) = ⊢-lsuc (⊢sub ⊢σ ⊢e) +⊢sub ⊢σ (⊢-⊔ ⊢l ⊢r) = ⊢-⊔ (⊢sub ⊢σ ⊢l) (⊢sub ⊢σ ⊢r) ⊢sub₁ : ∀ {n} {Γ : Context n} {e : Term n} {t} → Γ ⊢ e ⦂ t