From 077d91a485c506a4625091cc5bf38d2ab578b0cf Mon Sep 17 00:00:00 2001 From: JKF Date: Fri, 17 Apr 2026 19:31:44 +0200 Subject: [PATCH] changes --- SubjectReduction/Composition.agda | 36 ++++++-- SubjectReduction/Confluence.agda | 130 +++++++++++++++++++++++++--- SubjectReduction/Specification.agda | 15 ++-- 3 files changed, 158 insertions(+), 23 deletions(-) diff --git a/SubjectReduction/Composition.agda b/SubjectReduction/Composition.agda index aa52584..e66e7b8 100644 --- a/SubjectReduction/Composition.agda +++ b/SubjectReduction/Composition.agda @@ -32,7 +32,12 @@ ext-dist-∘ᵣᵣ ρ₁ ρ₂ = fun-ext eq fusion-∘ᵣᵣ : ∀ {n₁ n₂ n₃} (ρ₁ : Ren n₂ n₃) (ρ₂ : Ren n₁ n₂) (e : Term n₁) → ren ρ₁ (ren ρ₂ e) ≡ ren (ρ₁ ∘ᵣᵣ ρ₂) e fusion-∘ᵣᵣ ρ₁ ρ₂ (` x) = refl -fusion-∘ᵣᵣ ρ₁ ρ₂ `Set = refl +fusion-∘ᵣᵣ ρ₁ ρ₂ (`Setω e) = cong `Setω_ (fusion-∘ᵣᵣ ρ₁ ρ₂ e) +fusion-∘ᵣᵣ ρ₁ ρ₂ (`Setn e) = cong `Setn_ (fusion-∘ᵣᵣ ρ₁ ρ₂ e) +fusion-∘ᵣᵣ ρ₁ ρ₂ `Level = refl +fusion-∘ᵣᵣ ρ₁ ρ₂ `lzero = refl +fusion-∘ᵣᵣ ρ₁ ρ₂ (`lsuc e) = cong `lsuc (fusion-∘ᵣᵣ ρ₁ ρ₂ e) +fusion-∘ᵣᵣ ρ₁ ρ₂ (l `⊔ r) rewrite fusion-∘ᵣᵣ ρ₁ ρ₂ l | fusion-∘ᵣᵣ ρ₁ ρ₂ r = refl fusion-∘ᵣᵣ ρ₁ ρ₂ `refl = refl fusion-∘ᵣᵣ ρ₁ ρ₂ (∀[x⦂ x ] e) rewrite fusion-∘ᵣᵣ ρ₁ ρ₂ x | (fusion-∘ᵣᵣ (extᵣ ρ₁) (extᵣ ρ₂) e) | ext-dist-∘ᵣᵣ ρ₁ ρ₂ = refl @@ -70,7 +75,12 @@ ext-dist-∘ₛᵣ _ _ = fun-ext λ{zero → refl; (suc x) → refl } fusion-∘ₛᵣ : ∀ {n₁ n₂ n₃} (σ₁ : Sub n₂ n₃) (ρ₂ : Ren n₁ n₂) (e : Term n₁) → sub σ₁ (ren ρ₂ e) ≡ sub (σ₁ ∘ₛᵣ ρ₂) e fusion-∘ₛᵣ σ ρ (` x) = refl -fusion-∘ₛᵣ σ ρ `Set = refl +fusion-∘ₛᵣ σ ρ (`Setω e) rewrite fusion-∘ₛᵣ σ ρ e = refl +fusion-∘ₛᵣ σ ρ (`Setn e) rewrite fusion-∘ₛᵣ σ ρ e = refl +fusion-∘ₛᵣ σ ρ `Level = refl +fusion-∘ₛᵣ σ ρ `lzero = refl +fusion-∘ₛᵣ σ ρ (`lsuc e) rewrite fusion-∘ₛᵣ σ ρ e = refl +fusion-∘ₛᵣ σ ρ (l `⊔ r) rewrite fusion-∘ₛᵣ σ ρ l | fusion-∘ₛᵣ σ ρ r = refl fusion-∘ₛᵣ σ ρ `refl = refl fusion-∘ₛᵣ σ ρ (`λ e) rewrite fusion-∘ₛᵣ (extₛ σ) (extᵣ ρ) e | ext-dist-∘ₛᵣ σ ρ = refl fusion-∘ₛᵣ σ ρ (l · r) rewrite fusion-∘ₛᵣ σ ρ l | fusion-∘ₛᵣ σ ρ r = refl @@ -123,7 +133,13 @@ ext-dist-∘ᵣₛ ρ σ = fun-ext (fun-ext-aux₁ ρ σ) fusion-∘ᵣₛ : ∀ {n₁ n₂ n₃} (ρ₁ : Ren n₂ n₃) (σ₂ : Sub n₁ n₂) (e : Term n₁) → ren ρ₁ (sub σ₂ e) ≡ sub (ρ₁ ∘ᵣₛ σ₂) e fusion-∘ᵣₛ ρ σ (` x) = refl -fusion-∘ᵣₛ ρ σ `Set = refl +fusion-∘ᵣₛ ρ σ (`Setn e) rewrite fusion-∘ᵣₛ ρ σ e = refl +fusion-∘ᵣₛ ρ σ (`Setω e) rewrite fusion-∘ᵣₛ ρ σ e = refl +fusion-∘ᵣₛ ρ σ `Level = refl +fusion-∘ᵣₛ ρ σ `lzero = refl +fusion-∘ᵣₛ ρ σ (`lsuc e) rewrite fusion-∘ᵣₛ ρ σ e = refl +fusion-∘ᵣₛ ρ σ (l `⊔ r) rewrite fusion-∘ᵣₛ ρ σ l + | fusion-∘ᵣₛ ρ σ r = refl fusion-∘ᵣₛ ρ σ `refl = refl fusion-∘ᵣₛ ρ σ (`λ e) rewrite fusion-∘ᵣₛ (extᵣ ρ) (extₛ σ) e | ext-dist-∘ᵣₛ ρ σ = refl @@ -181,7 +197,12 @@ ext-dist-∘ₛₛ σ₁ σ₂ = fun-ext (fun-ext-aux₂ σ₁ σ₂) fusion-∘ₛₛ : ∀ {n₁ n₂ n₃} (σ₁ : Sub n₂ n₃) (σ₂ : Sub n₁ n₂) (e : Term n₁) → sub σ₁ (sub σ₂ e) ≡ sub (σ₁ ∘ₛₛ σ₂) e fusion-∘ₛₛ σ₁ σ₂ (` x) = refl -fusion-∘ₛₛ σ₁ σ₂ `Set = refl +fusion-∘ₛₛ σ₁ σ₂ (`Setn e) rewrite fusion-∘ₛₛ σ₁ σ₂ e = refl +fusion-∘ₛₛ σ₁ σ₂ (`Setω e) rewrite fusion-∘ₛₛ σ₁ σ₂ e = refl +fusion-∘ₛₛ σ₁ σ₂ `Level = refl +fusion-∘ₛₛ σ₁ σ₂ `lzero = refl +fusion-∘ₛₛ σ₁ σ₂ (`lsuc e) rewrite fusion-∘ₛₛ σ₁ σ₂ e = refl +fusion-∘ₛₛ σ₁ σ₂ (l `⊔ r) rewrite fusion-∘ₛₛ σ₁ σ₂ l | fusion-∘ₛₛ σ₁ σ₂ r = refl fusion-∘ₛₛ σ₁ σ₂ `refl = refl fusion-∘ₛₛ σ₁ σ₂ (`λ e) rewrite fusion-∘ₛₛ (extₛ σ₁) (extₛ σ₂) e | ext-dist-∘ₛₛ σ₁ σ₂ = refl fusion-∘ₛₛ σ₁ σ₂ (l · r) rewrite fusion-∘ₛₛ σ₁ σ₂ l | fusion-∘ₛₛ σ₁ σ₂ r = refl @@ -210,7 +231,12 @@ extₛ-idₛ {n} = fun-ext λ{zero → refl; (suc x) → refl} sub-id : ∀ {n} (e : Term n) → sub idₛ e ≡ e sub-id (` x) = refl -sub-id `Set = refl +sub-id (`Setn e) = cong (`Setn_) (trans (cong (λ a → sub a e) refl) (sub-id e)) +sub-id (`Setω e) = cong (`Setω_) (trans (cong (λ a → sub a e) refl) (sub-id e)) +sub-id (`lsuc e) = cong (`lsuc) (trans (cong (λ a → sub a e) refl) (sub-id e)) +sub-id `Level = refl +sub-id `lzero = refl +sub-id (l `⊔ r) rewrite sub-id l | sub-id r = refl sub-id `refl = refl sub-id (`λ e) = cong (λ a → `λ a) (trans (cong (λ a → sub a e) extₛ-idₛ) (sub-id e)) sub-id (`proj₁ e) = cong (λ a → `proj₁ a) (trans (cong (λ a → sub a e) refl) (sub-id e)) diff --git a/SubjectReduction/Confluence.agda b/SubjectReduction/Confluence.agda index ac29565..46673de 100644 --- a/SubjectReduction/Confluence.agda +++ b/SubjectReduction/Confluence.agda @@ -128,6 +128,41 @@ open import univTypes.Util.Fin using (Fin; zero; suc) → `subst t e₁ e₂ ↪* `subst t e₁ e₂' ξ*-subst₃ ↪*-refl = ↪*-refl ξ*-subst₃ (↪*-step ↪ ↪*) = ↪*-step (ξ-subst₃ ↪) (ξ*-subst₃ ↪* ) +-- New +ξ*-lsuc : ∀ {n} {x x' : Term n} + → x ↪* x' + ------------------------------- + → `lsuc x ↪* `lsuc x' +ξ*-lsuc ↪*-refl = ↪*-refl +ξ*-lsuc (↪*-step ↪ ↪*) = ↪*-step (ξ-lsuc ↪) (ξ*-lsuc ↪*) + +ξ*-Setω : ∀ {n} {x x' : Term n} + → x ↪* x' + ------------------------------- + → `Setω x ↪* `Setω x' +ξ*-Setω ↪*-refl = ↪*-refl +ξ*-Setω (↪*-step ↪ ↪*) = ↪*-step (ξ-Setω ↪) (ξ*-Setω ↪*) + +ξ*-Setn : ∀ {n} {x x' : Term n} + → x ↪* x' + ------------------------------- + → `Setn x ↪* `Setn x' +ξ*-Setn ↪*-refl = ↪*-refl +ξ*-Setn (↪*-step ↪ ↪*) = ↪*-step (ξ-Setn ↪) (ξ*-Setn ↪*) + +ξ*-⊔₁ : ∀ {n} {l l' r : Term n} + → l ↪* l' + ------------------------------- + → l `⊔ r ↪* l' `⊔ r +ξ*-⊔₁ ↪*-refl = ↪*-refl +ξ*-⊔₁ (↪*-step x l↪l') = ↪*-step (ξ-⊔₁ x) (ξ*-⊔₁ l↪l') + +ξ*-⊔₂ : ∀ {n} {l r r' : Term n} + → r ↪* r' + ------------------------------- + → l `⊔ r ↪* l `⊔ r' +ξ*-⊔₂ ↪*-refl = ↪*-refl +ξ*-⊔₂ (↪*-step x r↪r') = ↪*-step (ξ-⊔₂ x) (ξ*-⊔₂ r↪r') -------------------------------------------------------------------------------- -- Parallel Reduction @@ -182,10 +217,26 @@ data _↪ₚ_ : ∀ {n} → Term n → Term n → Set where β-subst : ∀ {n} {t : Term (suc n)} {e e' : Term n} → e ↪ₚ e' → `subst t `refl e ↪ₚ e' - ξ-Set : ∀ {n} → - `Set ↪ₚ (`Set {n = n}) ξ-refl : ∀ {n} → `refl ↪ₚ (`refl {n = n}) +-- New: + ξ-Setω : ∀ {n} {x x' : Term n} → + x ↪ₚ x' → + `Setω x ↪ₚ (`Setω x') + ξ-Setn : ∀ {n} {x x' : Term n} → + x ↪ₚ x' → + `Setn x ↪ₚ (`Setn x') + ξ-Level : ∀ {n} → + `Level ↪ₚ `Level {n = n} + ξ-lzero : ∀ {n} → + `lzero ↪ₚ `lzero {n = n} + ξ-lsuc : ∀ {n} {x x' : Term n} → + x ↪ₚ x' → + `lsuc x ↪ₚ `lsuc x' + ξ-⊔ : ∀ {n} {e₁ e₁' e₂ e₂' : Term n} → + e₁ ↪ₚ e₁' → + e₂ ↪ₚ e₂' → + e₁ `⊔ e₂ ↪ₚ e₁' `⊔ e₂' ↪ₚ₁ : ∀ {n} {fst snd : Term n} → (fst ↪ₚ snd) → Term n ↪ₚ₁ {n} {fst} {snd} _ = fst @@ -245,7 +296,6 @@ module ↪ₚ*-Reasoning where ↪ₚ-refl {n} {` x} = ξ-` ↪ₚ-refl {n} {`proj₁ t} = ξ-proj₁ ↪ₚ-refl ↪ₚ-refl {n} {`proj₂ t} = ξ-proj₂ ↪ₚ-refl -↪ₚ-refl {n} {`Set} = ξ-Set ↪ₚ-refl {n} {`λ t} = ξ-λ ↪ₚ-refl ↪ₚ-refl {n} {t · t₁} = ξ-· ↪ₚ-refl ↪ₚ-refl ↪ₚ-refl {n} {∀[x⦂ t ] t₁} = ξ-∀ ↪ₚ-refl ↪ₚ-refl @@ -253,6 +303,12 @@ module ↪ₚ*-Reasoning where ↪ₚ-refl {n} {t `, t₁} = ξ-, ↪ₚ-refl ↪ₚ-refl ↪ₚ-refl {n} {t `≡ t₁} = ξ-≡ ↪ₚ-refl ↪ₚ-refl ↪ₚ-refl {n} {`subst t t₁ t₂} = ξ-subst ↪ₚ-refl ↪ₚ-refl ↪ₚ-refl +↪ₚ-refl {n} {`Setω x} = ξ-Setω ↪ₚ-refl +↪ₚ-refl {n} {`Setn x} = ξ-Setn ↪ₚ-refl +↪ₚ-refl {n} {`Level} = ξ-Level +↪ₚ-refl {n} {`lzero} = ξ-lzero +↪ₚ-refl {n} {`lsuc x} = ξ-lsuc ↪ₚ-refl +↪ₚ-refl {n} {x `⊔ x₁} = ξ-⊔ ↪ₚ-refl ↪ₚ-refl -------------------------------------------------------------------------------- @@ -281,6 +337,12 @@ module ↪ₚ*-Reasoning where ↪→↪ₚ (ξ-subst₃ t↪t') = ξ-subst ↪ₚ-refl ↪ₚ-refl(↪→↪ₚ t↪t') ↪→↪ₚ β-proj₁ = β-proj₁ ↪ₚ-refl ↪→↪ₚ β-proj₂ = β-proj₂ ↪ₚ-refl +-- New +↪→↪ₚ (ξ-⊔₁ x) = ξ-⊔ (↪→↪ₚ x) ↪ₚ-refl +↪→↪ₚ (ξ-⊔₂ x) = ξ-⊔ ↪ₚ-refl (↪→↪ₚ x) +↪→↪ₚ (ξ-Setn x) = ξ-Setn (↪→↪ₚ x) +↪→↪ₚ (ξ-Setω x) = ξ-Setω (↪→↪ₚ x) +↪→↪ₚ (ξ-lsuc x) = ξ-lsuc (↪→↪ₚ x) ↪*→↪ₚ* : ∀ {n} {t t' : Term n} → t ↪* t' @@ -295,7 +357,6 @@ module ↪ₚ*-Reasoning where → t ↪ₚ t' → t ↪* t' ↪ₚ→↪* ξ-` = ↪*-refl -↪ₚ→↪* ξ-Set = ↪*-refl ↪ₚ→↪* (ξ-λ ↪₁) = ξ*-λ (↪ₚ→↪* ↪₁) ↪ₚ→↪* (ξ-∀ ↪₁ ↪₂) = b where @@ -336,6 +397,15 @@ module ↪ₚ*-Reasoning where e = ↪*-trans c d ↪ₚ→↪* (β-proj₁ x↪x') = ↪*-step β-proj₁ (↪ₚ→↪* x↪x') ↪ₚ→↪* (β-proj₂ x↪x') = ↪*-step β-proj₂ (↪ₚ→↪* x↪x') +↪ₚ→↪* (ξ-Setω x↪x') = ξ*-Setω (↪ₚ→↪* x↪x') +↪ₚ→↪* (ξ-Setn x↪x') = ξ*-Setn (↪ₚ→↪* x↪x') +↪ₚ→↪* ξ-Level = ↪*-refl +↪ₚ→↪* ξ-lzero = ↪*-refl +↪ₚ→↪* (ξ-lsuc x↪x') = ξ*-lsuc (↪ₚ→↪* x↪x') +↪ₚ→↪* (ξ-⊔ l↪l' r↪r') = ↪*-trans a b + where + a = ξ*-⊔₁ (↪ₚ→↪* l↪l') + b = ξ*-⊔₂ (↪ₚ→↪* r↪r') ↪ₚ*→↪* : ∀ {n} {t t' : Term n} → t ↪ₚ* t' @@ -361,7 +431,6 @@ module ↪ₚ*-Reasoning where ↪ₚ-ren ρ (ξ-λ ↪) = ξ-λ (↪ₚ-ren (extᵣ ρ) ↪) ↪ₚ-ren ρ (ξ-∀ ↪₁ ↪₂) = ξ-∀ (↪ₚ-ren ρ ↪₁) (↪ₚ-ren (extᵣ ρ) ↪₂) ↪ₚ-ren ρ (ξ-· ↪₁ ↪₂) = ξ-· (↪ₚ-ren ρ ↪₁) (↪ₚ-ren ρ ↪₂) -↪ₚ-ren ρ ξ-Set = ξ-Set ↪ₚ-ren ρ (ξ-proj₁ t↪t') = ξ-proj₁ (↪ₚ-ren ρ t↪t') ↪ₚ-ren ρ (ξ-proj₂ t↪t') = ξ-proj₂ (↪ₚ-ren ρ t↪t') ↪ₚ-ren ρ (ξ-∃ t↪t' t↪t'') = ξ-∃ (↪ₚ-ren ρ t↪t') (↪ₚ-ren (extᵣ ρ) t↪t'') @@ -372,8 +441,14 @@ module ↪ₚ*-Reasoning where ↪ₚ-ren ρ ξ-refl = ξ-refl ↪ₚ-ren ρ (β-proj₁ x↪x') = β-proj₁ (↪ₚ-ren ρ x↪x') ↪ₚ-ren ρ (β-proj₂ x↪x') = β-proj₂ (↪ₚ-ren ρ x↪x') +↪ₚ-ren ρ (ξ-Setω x) = ξ-Setω (↪ₚ-ren ρ x) +↪ₚ-ren ρ (ξ-Setn x) = ξ-Setn (↪ₚ-ren ρ x) +↪ₚ-ren ρ ξ-Level = ξ-Level +↪ₚ-ren ρ ξ-lzero = ξ-lzero +↪ₚ-ren ρ (ξ-lsuc x) = ξ-lsuc (↪ₚ-ren ρ x) +↪ₚ-ren ρ (ξ-⊔ l r) = ξ-⊔ (↪ₚ-ren ρ l) (↪ₚ-ren ρ r) --------{! !}----------------------------------------------------------------------- +------------------------------------------------------------------------------ -- A substitution σ₁ reduces to σ₂, if each term of σ₁ reduces to the -- corresponding term of σ₂. @@ -402,7 +477,6 @@ _↪ₚσ_ : ∀ {m n} (σ₁ σ₂ : Sub m n) → Set ↪ₚσ-sub ↪σ (ξ-· l↪ₚl' r↪ₚr') = ξ-· (↪ₚσ-sub ↪σ l↪ₚl') (↪ₚσ-sub ↪σ r↪ₚr') ↪ₚσ-sub ↪σ (ξ-≡ l↪ₚl' r↪ₚr') = ξ-≡ (↪ₚσ-sub ↪σ l↪ₚl') (↪ₚσ-sub ↪σ r↪ₚr') ↪ₚσ-sub ↪σ (ξ-, l↪ₚl' r↪ₚr') = ξ-, (↪ₚσ-sub ↪σ l↪ₚl') (↪ₚσ-sub ↪σ r↪ₚr') -↪ₚσ-sub ↪σ ξ-Set = ξ-Set ↪ₚσ-sub {σ' = σ'} ↪σ (β-λ ₁↪ₚ ₂↪ₚ) = ↪ₚ-≡ (β-λ (↪ₚσ-sub (↪ₚσ-ext ↪σ) ₁↪ₚ) (↪ₚσ-sub ↪σ ₂↪ₚ)) (swap-0↦-extₛ-fusion σ' (↪ₚ₂ ₂↪ₚ) (↪ₚ₂ ₁↪ₚ)) ↪ₚσ-sub ↪σ (ξ-proj₁ e↪ₚe') = ξ-proj₁ (↪ₚσ-sub ↪σ e↪ₚe') @@ -411,6 +485,12 @@ _↪ₚσ_ : ∀ {m n} (σ₁ σ₂ : Sub m n) → Set ↪ₚσ-sub ↪σ (β-subst e↪e') = β-subst (↪ₚσ-sub ↪σ e↪e') ↪ₚσ-sub ↪σ (β-proj₁ x) = β-proj₁ (↪ₚσ-sub ↪σ x) ↪ₚσ-sub ↪σ (β-proj₂ x) = β-proj₂ (↪ₚσ-sub ↪σ x) +↪ₚσ-sub ↪σ (ξ-Setω x) = ξ-Setω (↪ₚσ-sub ↪σ x) +↪ₚσ-sub ↪σ (ξ-Setn x) = ξ-Setn (↪ₚσ-sub ↪σ x) +↪ₚσ-sub ↪σ ξ-Level = ξ-Level +↪ₚσ-sub ↪σ ξ-lzero = ξ-lzero +↪ₚσ-sub ↪σ (ξ-lsuc x) = ξ-lsuc (↪ₚσ-sub ↪σ x) +↪ₚσ-sub ↪σ (ξ-⊔ x x₁) = ξ-⊔ (↪ₚσ-sub ↪σ x) (↪ₚσ-sub ↪σ x₁) ↪ₚσ-0↦ : ∀ {n} {e₁ e₂ : Term n} → e₁ ↪ₚ e₂ → @@ -435,7 +515,6 @@ _⁺ : ∀ {n} → Term n → Term n (e₁ `≡ e₂) ⁺ = (e₁ ⁺) `≡ (e₂ ⁺) (∀[x⦂ t₁ ] t₂) ⁺ = ∀[x⦂ (t₁ ⁺) ] (t₂ ⁺) (∃[x⦂ t₁ ] t₂) ⁺ = ∃[x⦂ (t₁ ⁺) ] (t₂ ⁺) -`Set ⁺ = `Set `refl ⁺ = `refl `proj₁ (e `, _) ⁺ = (e ⁺) `proj₂ (_ `, e) ⁺ = (e ⁺) @@ -443,6 +522,12 @@ _⁺ : ∀ {n} → Term n → Term n `proj₂ e ⁺ = `proj₂ (e ⁺) (`subst t `refl e) ⁺ = (e ⁺) (`subst t e₁ e₂) ⁺ = `subst (t ⁺) (e₁ ⁺) (e₂ ⁺) +(`Setω x) ⁺ = `Setω (x ⁺) +(`Setn x) ⁺ = `Setn (x ⁺) +`Level ⁺ = `Level +`lzero ⁺ = `lzero +`lsuc x ⁺ = `lsuc (x ⁺) +(x `⊔ x₁) ⁺ = (x ⁺) `⊔ (x₁ ⁺) -- Note, in part 4, this proof might have *many* cases. That's to be -- expected, and most of them are actually very similar. @@ -452,7 +537,6 @@ par-triangle : ∀ {n} {e e' : Term n} ------- → e' ↪ₚ (e ⁺) par-triangle ξ-` = ξ-` -par-triangle ξ-Set = ξ-Set par-triangle ξ-refl = ξ-refl par-triangle (β-λ ₁↪ₚ ₂↪ₚ) = ↪ₚσ-[] (par-triangle ₁↪ₚ) (par-triangle ₂↪ₚ) par-triangle (ξ-λ x) = ξ-λ (par-triangle x) @@ -462,7 +546,6 @@ par-triangle (ξ-· (ξ-∀ ll lr) r) = ξ-· (ξ-∀ (par-triangle ll) (par-tri par-triangle (ξ-· ξ-` r) = ξ-· ξ-` (par-triangle r) par-triangle (ξ-· (ξ-λ l) r) = β-λ (par-triangle l) (par-triangle r) par-triangle (ξ-· (ξ-· ll lr) r) = ξ-· (par-triangle (ξ-· ll lr)) (par-triangle r) -par-triangle (ξ-· ξ-Set r) = ξ-· ξ-Set (par-triangle r) par-triangle (ξ-· p@(β-proj₁ l) r) = ξ-· (par-triangle p) (par-triangle r) par-triangle (ξ-· p@(β-proj₂ l) r) = ξ-· (par-triangle p) (par-triangle r) par-triangle (ξ-· (ξ-proj₁ l) r) = ξ-· (par-triangle (ξ-proj₁ l)) (par-triangle r) @@ -489,7 +572,6 @@ par-triangle (ξ-proj₁ (ξ-≡ e e₁)) = ξ-proj₁ (ξ-≡ (par-triangle e) par-triangle (ξ-proj₁ (ξ-, e e₁)) = β-proj₁ (par-triangle e) par-triangle (ξ-proj₁ (ξ-subst e e₁ e₂)) = ξ-proj₁ (par-triangle (ξ-subst e e₁ e₂)) par-triangle (ξ-proj₁ (β-subst e)) = ξ-proj₁ (par-triangle e) -par-triangle (ξ-proj₁ ξ-Set) = ξ-proj₁ ξ-Set par-triangle (ξ-proj₁ ξ-refl) = ξ-proj₁ ξ-refl par-triangle (ξ-proj₂ ξ-`) = ξ-proj₂ ξ-` par-triangle (ξ-proj₂ (β-proj₁ e)) = ξ-proj₂ (par-triangle e) @@ -505,7 +587,6 @@ par-triangle (ξ-proj₂ (ξ-≡ e e₁)) = ξ-proj₂ (ξ-≡ (par-triangle e) par-triangle (ξ-proj₂ (ξ-, e e₁)) = β-proj₂ (par-triangle e₁) par-triangle (ξ-proj₂ (ξ-subst e e₁ e₂)) = ξ-proj₂ (par-triangle (ξ-subst e e₁ e₂)) par-triangle (ξ-proj₂ (β-subst e)) = ξ-proj₂ (par-triangle e) -par-triangle (ξ-proj₂ ξ-Set) = ξ-proj₂ ξ-Set par-triangle (ξ-proj₂ ξ-refl) = ξ-proj₂ ξ-refl par-triangle (ξ-∃ e e₁) = ξ-∃ (par-triangle e) (par-triangle e₁) par-triangle (ξ-≡ e e₁) = ξ-≡ (par-triangle e) (par-triangle e₁) @@ -525,8 +606,31 @@ par-triangle (ξ-subst e (ξ-≡ e₁ e₃) e₂) = ξ-subst (par-triangle e) ( par-triangle (ξ-subst e (ξ-, e₁ e₃) e₂) = ξ-subst (par-triangle e) (ξ-, (par-triangle e₁) (par-triangle e₃)) (par-triangle e₂) par-triangle (ξ-subst e (ξ-subst e₁ e₃ e₄) e₂) = ξ-subst (par-triangle e) (par-triangle (ξ-subst e₁ e₃ e₄)) (par-triangle e₂) par-triangle (ξ-subst e (β-subst e₁) e₂) = ξ-subst (par-triangle e) (par-triangle e₁) (par-triangle e₂) -par-triangle (ξ-subst e ξ-Set e₂) = ξ-subst (par-triangle e) ξ-Set (par-triangle e₂) par-triangle (ξ-subst e ξ-refl e₂) = β-subst (par-triangle e₂) +par-triangle (ξ-proj₁ (ξ-Setω x)) = ξ-proj₁ (ξ-Setω (par-triangle x)) +par-triangle (ξ-proj₁ (ξ-Setn x)) = ξ-proj₁ (ξ-Setn (par-triangle x)) +par-triangle (ξ-proj₁ ξ-Level) = ξ-proj₁ ξ-Level +par-triangle (ξ-proj₁ ξ-lzero) = ξ-proj₁ (par-triangle ξ-lzero) +par-triangle (ξ-proj₁ (ξ-lsuc x)) = ξ-proj₁ (ξ-lsuc (par-triangle x)) +par-triangle (ξ-proj₁ (ξ-⊔ x x₁)) = ξ-proj₁ (ξ-⊔ (par-triangle x) (par-triangle x₁)) +par-triangle (ξ-proj₂ (ξ-Setω x)) = ξ-proj₂ (ξ-Setω (par-triangle x)) +par-triangle (ξ-proj₂ (ξ-Setn x)) = ξ-proj₂ (ξ-Setn (par-triangle x)) +par-triangle (ξ-proj₂ ξ-Level) = ξ-proj₂ ξ-Level +par-triangle (ξ-proj₂ ξ-lzero) = ξ-proj₂ (par-triangle ξ-lzero) +par-triangle (ξ-proj₂ (ξ-lsuc x)) = ξ-proj₂ (ξ-lsuc (par-triangle x)) +par-triangle (ξ-proj₂ (ξ-⊔ x x₁)) = ξ-proj₂ (ξ-⊔ (par-triangle x) (par-triangle x₁)) +par-triangle (ξ-· x x₁) = {! !} +par-triangle (ξ-subst x x₁ x₂) = {! !} +par-triangle (ξ-Setω x) = ξ-Setω (par-triangle x) +par-triangle (ξ-Setn x) = ξ-Setn (par-triangle x) +par-triangle ξ-Level = ξ-Level +par-triangle ξ-lzero = ξ-lzero +par-triangle (ξ-lsuc x) = ξ-lsuc (par-triangle x) +par-triangle (ξ-⊔ x x₁) = ξ-⊔ (par-triangle x) (par-triangle x₁) +-- par-triangle (ξ-proj₁ ξ-Set) = ξ-proj₁ ξ-Set +-- par-triangle (ξ-proj₂ ξ-Set) = ξ-proj₂ ξ-Set +-- par-triangle (ξ-· ξ-Set r) = ξ-· ξ-Set (par-triangle r) +-- par-triangle (ξ-subst e ξ-Set e₂) = ξ-subst (par-triangle e) ξ-Set (par-triangle e₂) 1→* : ∀ {m} {e e' : Term m} → e ↪ₚ e' → (e ↪ₚ* e') 1→* e↪ₚe' = ↪ₚ*-step e↪ₚe' ↪ₚ*-refl diff --git a/SubjectReduction/Specification.agda b/SubjectReduction/Specification.agda index a79a407..e4dc349 100644 --- a/SubjectReduction/Specification.agda +++ b/SubjectReduction/Specification.agda @@ -37,8 +37,8 @@ data Term : ℕ → Set where `Setω_ : ∀ {n} (l : Term n) → Term n `Setn_ : ∀ {n} (l : Term n) → Term n `Level : ∀ {n} → Term n - `lzero : ∀ {n} → Term n - `lsuc : ∀ {n} → Term n → Term n + `lzero : ∀ {n} → Term n + `lsuc : ∀ {n} → Term n → Term n _`⊔_ : ∀ {n} → Term n → Term n → Term n -- Extension @@ -149,10 +149,10 @@ mutual val-Level : ∀ {n} → Value {n = n} `Level - val-l : ∀ {n v} + val-l : ∀ {n} → Value {n = n} (`lzero) - val-lsuc : ∀ {n v l} + val-lsuc : ∀ {n l} → Value l → Value {n = n} (`lsuc l) @@ -289,7 +289,7 @@ data _↪_ : ∀ {n} → Term n → Term n → Set where → e₂ ↪ e₂' → `subst t e₁ e₂ ↪ `subst t e₁ e₂' --- Extension: +-- New ξ-⊔₁ : ∀ {n} {t₁ t₁' : Term n} {t₂ : Term n} → t₁ ↪ t₁' ------------------------------- @@ -300,6 +300,10 @@ data _↪_ : ∀ {n} → Term n → Term n → Set where ------------------------------- → (t₁ `⊔ t₂) ↪ (t₁ `⊔ t₂') + ξ-lsuc : ∀ {n} {l l' : Term n} + → l ↪ l' + → `lsuc l ↪ `lsuc l' + ξ-Setn : ∀ {n} {l l' : Term n} → l ↪ l' → `Setn l ↪ `Setn l' @@ -467,3 +471,4 @@ data _⊢_⦂_ : ∀ {n} → Context n → Term n → Term n → Set where cong₃ : ∀ {A B C D : Set} (f : A → B → C → D) {x y u v a b} → x ≡ y → u ≡ v → a ≡ b → f x u a ≡ f y v b cong₃ f refl refl refl = refl +