minze/univTypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

small work

Browse Source
This commit is contained in:
Julius
2026-04-21 20:44:15 +02:00
parent 077d91a485
commit 5cbf679c0c
2 changed files with 56 additions and 12 deletions
Download Patch File Download Diff File Expand all files Collapse all files
SubjectReduction/ConversionProperties.agda
+43 -6
View File
@@ -65,7 +65,6 @@ open import univTypes.Util.Fin
→ e ↪ₚ* e'
---------------
→ `proj₂ e ↪ₚ* `proj₂ e'
ξₚ*-proj₂ e↪ₚ*e' = ↪*→↪ₚ* (ξ*-proj₂ (↪ₚ*→↪* e↪ₚ*e'))
ξₚ*-· : ∀ {n} {e₁ e₂ e₁' e₂' : Term n}
@@ -126,6 +125,15 @@ open import univTypes.Util.Fin
ξ-2 = ξ*-subst₃ (↪ₚ*→↪* e₂↪ₚ*e₂')
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'))
--------------------------------------------------------------------------------
-- "Substituting two convertible terms into another term, yields again convertible terms."
@@ -160,7 +168,6 @@ _≈σ_ : ∀ {m n} (σ₁ σ₂ : Sub m n) → Set
↪ₚ*σ-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 σ↪σ'))
@@ -173,6 +180,12 @@ _≈σ_ : ∀ {m n} (σ₁ σ₂ : Sub m n) → Set
↪ₚ*σ-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} {`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} {e : Term m} {σ σ' : Sub m n} →
σ ↪*σ σ' →
@@ -190,7 +203,6 @@ ext-≈σ ≈ₛ (suc x) with ≈ₛ x
→ σ ≈σ σ'
→ 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'
@@ -219,6 +231,8 @@ 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} ≈σ' = {! !}
≈→≈σ : ∀ {n} {e e' : Term n}
→ e ≈ e'
@@ -273,6 +287,12 @@ ext-≈σ ≈ₛ (suc x) with ≈ₛ x
↪-ren ρ (ξ-subst₁ x) = ξ-subst₁ (↪-ren (extᵣ ρ) 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) = {! !}
-- Renaming preserves many reduction steps
@@ -314,7 +334,13 @@ ext-≈σ ≈ₛ (suc x) with ≈ₛ x
↪-sub σ (ξ-≡₂ x) = ξ-≡₂ (↪-sub σ x)
↪-sub σ (ξ-subst₁ x) = ξ-subst₁ (↪-sub (extₛ σ) x)
↪-sub σ (ξ-subst₂ x) = ξ-subst₂ (↪-sub σ x)
↪-sub σ (ξ-subst₃ x) = ξ-subst₃ (↪-sub σ x)
-- New
↪-sub σ (ξ-⊔₁ x) = {! !}
↪-sub σ (ξ-⊔₂ x) = {! !}
↪-sub σ (ξ-lsuc x) = {! !}
↪-sub σ (ξ-Setn x) = {! !}
↪-sub σ (ξ-subst₃ x) = {! !}
↪-sub σ (ξ-Setω x) = {! !}
-- Substitution preserves many reduction steps
@@ -363,19 +389,24 @@ _≈ᶜ_ : ∀ {n} → Context n → Context n → Set
≈-Γ-⊢ Γ₁≈Γ₂ (⊢-≡ ⊢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₁])
-- New
≈-Γ-⊢ Γ₁≈Γ₂ ⊢-Setn = {! !}
≈-Γ-⊢ Γ₁≈Γ₂ ⊢-Setω = {! !}
≈-Γ-⊢ Γ₁≈Γ₂ ⊢-lzero = {! !}
≈-Γ-⊢ Γ₁≈Γ₂ (⊢-lsuc ⊢x) = {! !}
≈-Γ-⊢ Γ₁≈Γ₂ (⊢-⊔ ⊢x ⊢x₁) = {! !}
≈-Γ-⊢ Γ₁≈Γ₂ ⊢-Level = {! !}
≈-Γ-⊢₁ : ∀ {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₃))
@@ -393,3 +424,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 = {! !}