changes

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