### changeset 344:e0916a632971

possible order restriction makes ω ZFSet
author Shinji KONO Mon, 13 Jul 2020 14:45:57 +0900 34e71402d579 f895642a8460 OD.agda 1 files changed, 7 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
```--- a/OD.agda	Mon Jul 13 14:30:37 2020 +0900
+++ b/OD.agda	Mon Jul 13 14:45:57 2020 +0900
@@ -106,7 +106,7 @@
postulate  odAxiom : ODAxiom
open ODAxiom odAxiom

--- possible restriction
+-- possible order restriction
hod-ord< :  {x : HOD } → Set n
hod-ord< {x} =  od→ord x o< next (odmax x)

@@ -237,6 +237,12 @@
lemmab1 : od→ord (x , x) o< next ( odmax (x , x))
lemmab1 = ho<

+pair<y : {x y : HOD } → y ∋ x  → od→ord (x , x) o< osuc (od→ord y)
+pair<y {x} {y} y∋x = ⊆→o≤ lemma where
+   lemma : {z : Ordinal} → def (od (x , x)) z → def (od y) z
+   lemma (case1 refl) = y∋x
+   lemma (case2 refl) = y∋x
+
-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
-- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)

@@ -259,12 +265,6 @@
od⊆→o≤ {x} {y} lt  =  ⊆→o≤ {x} {y} (λ {z} x>z  → subst (λ k → def (od y) k ) diso (incl lt (subst (λ k → def (od x) k ) (sym diso) x>z )))

-- if we have od→ord (x , x) ≡ osuc (od→ord x),  ⊆→o≤ → c<→o<
-pair<y : {x y : HOD } → y ∋ x  → od→ord (x , x) o< osuc (od→ord y)
-pair<y {x} {y} y∋x = ⊆→o≤ lemma where
-   lemma : {z : Ordinal} → def (od (x , x)) z → def (od y) z
-   lemma (case1 refl) = y∋x
-   lemma (case2 refl) = y∋x
-
⊆→o≤→c<→o< : ({x : HOD} → od→ord (x , x) ≡ osuc (od→ord x) )
→  ({y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) )
→   {x y : HOD  }   → def (od y) ( od→ord x ) → od→ord x o< od→ord y
@@ -394,14 +394,6 @@
lemma (isuc {y} x) = lemma2 where
lemma0 : y o< next o∅
lemma0 = lemma x
-            lemma3 : odef (u y ) y
-            lemma3 = FExists _ (λ {z} t not → not (od→ord (ord→od y , ord→od y)) record { proj1 = case2 refl ; proj2 = lemma4 }) (λ not → not y (infinite-d y)) where
-                lemma4 : def (od (ord→od (od→ord (ord→od y , ord→od y)))) y
-                lemma4 = subst₂ ( λ j k → def (od j) k ) (sym oiso) diso (case1 refl)
-            lemma5 : y o< odmax (u y)
-            lemma5 = <odmax (u y) lemma3
-            lemma6 : y o< odmax (ord→od y , (ord→od y , ord→od y))
-            lemma6 = <odmax (ord→od y , (ord→od y , ord→od y)) (subst ( λ k → def (od (ord→od y , (ord→od y , ord→od y))) k ) diso (case1 refl))
lemma8 : od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y))
lemma8 = ho<
---           (x,y) < next (omax x y) < next (osuc y) = next y
@@ -409,8 +401,6 @@
lemmaa {x} {y} x<y = subst (λ k → od→ord (x , y) o< k ) (sym nexto≡) (subst (λ k → od→ord (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< )
lemma81 : od→ord (ord→od y , ord→od y) o< next (od→ord (ord→od y))
lemma81 = nexto=n (subst (λ k →  od→ord (ord→od y , ord→od y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
-            lemma91 : od→ord (ord→od y) o< od→ord (ord→od y , ord→od y)
-            lemma91 = c<→o< (case1 refl)
lemma9 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y , ord→od y))
lemma9 = lemmaa (c<→o< (case1 refl))
lemma71 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y))```