Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1300:47d3cc596d68

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove next
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 04 Jun 2023 16:58:39 +0900
parents 054c2b0925c4
children 9e26c9abfafb
files src/BAlgebra.agda src/LEMC.agda src/OD.agda src/ODC.agda src/ODUtil.agda src/OrdUtil.agda src/Ordinals.agda src/PFOD.agda src/Topology.agda src/Tychonoff.agda src/VL.agda src/ZProduct.agda src/cardinal.agda src/filter-util.agda src/filter.agda src/generic-filter.agda src/maximum-filter.agda src/ordinal.agda src/zorn.agda
diffstat 19 files changed, 186 insertions(+), 151 deletions(-) [+]
line wrap: on
line diff
--- a/src/BAlgebra.agda	Sat Jun 03 17:31:28 2023 +0900
+++ b/src/BAlgebra.agda	Sun Jun 04 16:58:39 2023 +0900
@@ -22,7 +22,7 @@
 open inOrdinal O
 open Ordinals.Ordinals  O
 open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
+-- open Ordinals.IsNext isNext
 open OrdUtil O
 open ODUtil O
 
--- a/src/LEMC.agda	Sat Jun 03 17:31:28 2023 +0900
+++ b/src/LEMC.agda	Sun Jun 04 16:58:39 2023 +0900
@@ -23,7 +23,7 @@
 import ODUtil
 open Ordinals.Ordinals  O
 open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
+-- open Ordinals.IsNext isNext
 open OrdUtil O
 open ODUtil O
 
--- a/src/OD.agda	Sat Jun 03 17:31:28 2023 +0900
+++ b/src/OD.agda	Sun Jun 04 16:58:39 2023 +0900
@@ -18,7 +18,7 @@
 
 open Ordinals.Ordinals  O
 open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
+-- open Ordinals.IsNext isNext
 open OrdUtil O
 
 -- Ordinal Definable Set
@@ -54,7 +54,6 @@
 eq→ ( ⇔→==  {x} {y}  eq ) {z} m = proj1 eq m
 eq← ( ⇔→==  {x} {y}  eq ) {z} m = proj2 eq m
 
--- next assumptions are our axiom
 --
 --  OD is an equation on Ordinals, so it contains Ordinals. If these Ordinals have one-to-one
 --  correspondence to the OD then the OD looks like a ZF Set.
@@ -106,7 +105,7 @@
 postulate  odAxiom : ODAxiom
 open ODAxiom odAxiom
 
--- possible order restriction (required in the axiom of infinite )
+-- possible order restriction (required in the axiom of Omega )
 
 -- postulate  odAxiom-ho< : ODAxiom-ho<
 -- open ODAxiom-ho< odAxiom-ho<
@@ -443,41 +442,83 @@
 Intersection : (X : HOD ) → HOD   -- ∩ X
 Intersection X = record { od = record { def = λ x → (x o≤ & X ) ∧ ( {y : Ordinal} → odef X y → odef (* y) x )} ; odmax = osuc (& X) ; <odmax = λ lt → proj1 lt } 
 
+empty : (x : HOD  ) → ¬  (od∅ ∋ x)
+empty x = ¬x<0
+
 
 -- ｛_｝ : ZFSet → ZFSet
 -- ｛ x ｝ = ( x ,  x )     -- better to use (x , x) directly
 
-data infinite-d  : ( x : Ordinal  ) → Set n where
-    iφ :  infinite-d o∅
-    isuc : {x : Ordinal  } →   infinite-d  x  →
-            infinite-d  (& ( Union (* x , (* x , * x ) ) ))
+data Omega-d  : ( x : Ordinal  ) → Set n where
+    iφ :  Omega-d o∅
+    isuc : {x : Ordinal  } →   Omega-d  x  →
+            Omega-d  (& ( Union (* x , (* x , * x ) ) ))
 
 -- ω can be diverged in our case, since we have no restriction on the corresponding ordinal of a pair.
--- We simply assumes infinite-d y has a maximum.
+-- We simply assumes Omega-d y has a maximum.
 --
 -- This means that many of OD may not be HODs because of the & mapping divergence.
--- We should have some axioms to prevent this such as & x o< next (odmax x).
+-- We should have some axioms to prevent this .
 --
---  Since we have Ord (next o∅), we don't need this, but ZF axiom requires this and ho<
+
+Omega-od : OD
+Omega-od = record { def = λ x → Omega-d x } 
+
+o∅<x : {x : Ordinal} → o∅ o≤ x
+o∅<x {x} with trio< o∅ x
+... | tri< a ¬b ¬c = o<→≤ a
+... | tri≈ ¬a b ¬c = o≤-refl0 b
+... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
 
-infinite-od : OD
-infinite-od = record { def = λ x → infinite-d x } 
+¬0=ux : {x : HOD} → ¬ o∅ ≡ & (Union ( x , ( x ,  x)))
+¬0=ux {x} eq = ⊥-elim ( o<¬≡ eq (ordtrans≤-< o∅<x (subst (λ k → k o< & (Union (x , (x , x)))) &iso (c<→o< lemma ) ))) where
+    lemma : Own (x , (x , x)) (& ( * (& x )))
+    lemma = record { owner = _ ; ao = case2 refl ; ox = subst₂ (λ j k → odef j k ) (sym *iso) (sym &iso) (case1 refl) }
 
+ux-2cases : {x y : HOD } → Union ( x , ( x ,  x)) ∋ y → ( x ≡ y ) ∨ ( x ∋ y )
+ux-2cases {x} {y} record { owner = owner ; ao = (case1 eq) ; ox = ox } = case2 (subst (λ k → odef k (& y)) (trans (cong (*) eq) *iso) ox)
+ux-2cases {x} {y} record { owner = owner ; ao = (case2 eq) ; ox = ox } with subst (λ k → odef k (& y))  (trans (cong (*) eq) *iso) ox
+... | case1 eq = case1 (sym (&≡&→≡ eq))
+... | case2 eq = case1 (sym (&≡&→≡ eq))
+
+ux-transitve  : {x y : HOD} → x ∋ y →  Union ( x , ( x ,  x)) ∋ y 
+ux-transitve {x} {y} ox  = record { owner = _ ; ao = case1 refl ; ox = subst (λ k → odef k (& y)) (sym *iso) ox }
+
+--
+-- Possible Ordinal Limit
+--
+
+--        our Ordinals is greater than Union ( x , ( x ,  x)) transitive closure
+--
 record ODAxiom-ho< : Set (suc n) where
  field
     omega : Ordinal  
-    ho< : {x : Ordinal } → infinite-d x →  x o< next omega
+    ho< : {x : Ordinal } → Omega-d x →  x o< omega
 
 postulate
     odaxion-ho< : ODAxiom-ho< 
 
 open ODAxiom-ho< odaxion-ho<
 
-infinite : HOD
-infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next omega ; <odmax = ho<}  
+Omega : HOD
+Omega = record { od = record { def = λ x → Omega-d x } ; odmax = omega ; <odmax = ho<}  
 
-empty : (x : HOD  ) → ¬  (od∅ ∋ x)
-empty x = ¬x<0
+infinity∅ : Omega  ∋ od∅
+infinity∅ = subst (λ k → odef Omega k ) lemma iφ where
+    lemma : o∅ ≡ & od∅
+    lemma =  let open ≡-Reasoning in begin
+        o∅
+        ≡⟨ sym &iso ⟩
+        & ( * o∅ )
+        ≡⟨ cong ( λ k → & k ) o∅≡od∅ ⟩
+        & od∅
+        ∎
+
+infinity : (x : HOD) → Omega ∋ x → Omega ∋ Union (x , (x , x ))
+infinity x lt = subst (λ k → odef Omega k ) lemma (isuc {& x} lt) where
+    lemma :  & (Union (* (& x) , (* (& x) , * (& x))))
+        ≡ & (Union (x , (x , x)))
+    lemma = cong (λ k → & (Union ( k , ( k , k ) ))) *iso
 
 pair→ : ( x y t : HOD  ) →  (x , y)  ∋ t  → ( t =h= x ) ∨ ( t =h= y )
 pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j =h= k ) *iso *iso (o≡→== t≡x ))
@@ -529,22 +570,6 @@
 proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d
 proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d
 
-infinity∅ : infinite  ∋ od∅
-infinity∅ = subst (λ k → odef infinite k ) lemma iφ where
-    lemma : o∅ ≡ & od∅
-    lemma =  let open ≡-Reasoning in begin
-        o∅
-        ≡⟨ sym &iso ⟩
-        & ( * o∅ )
-        ≡⟨ cong ( λ k → & k ) o∅≡od∅ ⟩
-        & od∅
-        ∎
-infinity : (x : HOD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
-infinity x lt = subst (λ k → odef infinite k ) lemma (isuc {& x} lt) where
-    lemma :  & (Union (* (& x) , (* (& x) , * (& x))))
-        ≡ & (Union (x , (x , x)))
-    lemma = cong (λ k → & (Union ( k , ( k , k ) ))) *iso
-
 open import zf
 
 record ODAxiom-sup : Set (suc n) where
@@ -577,7 +602,7 @@
 zf-replacement→ : (os : ODAxiom-sup ) → {ψ : HOD → HOD} (X x : HOD) → (lt : ZFReplace os X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
 zf-replacement→ os {ψ} X x lt eq = eq (* (Replaced.z lt)) (ord→== (Replaced.x=ψz lt)) 
 
-isZF : (os : ODAxiom-sup) → IsZF HOD _∋_  _=h=_ od∅ _,_ Union Power Select (ZFReplace os) infinite
+isZF : (os : ODAxiom-sup) → IsZF HOD _∋_  _=h=_ od∅ _,_ Union Power Select (ZFReplace os) Omega
 isZF os = record {
         isEquivalence  = record { refl = ==-refl ; sym = ==-sym; trans = ==-trans }
     ;   pair→  = pair→
@@ -607,7 +632,7 @@
     ; Power = Power
     ; Select = Select
     ; Replace = ZFReplace os
-    ; infinite = infinite
+    ; infinite = Omega
     ; isZF = isZF os
  }
 
--- a/src/ODC.agda	Sat Jun 03 17:31:28 2023 +0900
+++ b/src/ODC.agda	Sun Jun 04 16:58:39 2023 +0900
@@ -26,7 +26,7 @@
 
 open Ordinals.Ordinals  O
 open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
+-- open Ordinals.IsNext isNext
 open OrdUtil O
 
 
--- a/src/ODUtil.agda	Sat Jun 03 17:31:28 2023 +0900
+++ b/src/ODUtil.agda	Sun Jun 04 16:58:39 2023 +0900
@@ -15,7 +15,7 @@
 
 open Ordinals.Ordinals  O
 open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
+-- open Ordinals.IsNext isNext
 import OrdUtil
 open OrdUtil O
 
@@ -81,7 +81,7 @@
 -- ... | tri> ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho<
 -- ... | tri≈ ¬a b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho<
 
---  another form of infinite
+--  another form of Omega
 -- pair-ord< :  {x : Ordinal } → Set n
 -- pair-ord< : {x : HOD } → ( {y : HOD } → & y o< next (odmax y) ) → & ( x , x ) o< next (& x)
 -- pair-ord< {x} ho< = subst (λ k → & (x , x) o< k ) lemmab0 lemmab1  where
@@ -120,23 +120,23 @@
 --
 --open ODAxiom-ho< odaxion-ho<
 
--- ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next omega
--- ω<next-o∅ {y} lt = <odmax infinite lt
+-- ω<next-o∅ : {y : Ordinal} → Omega-d y → y o< next omega
+-- ω<next-o∅ {y} lt = <odmax Omega lt
 
 nat→ω : Nat → HOD
 nat→ω Zero = od∅
 nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y))
 
-ω→nato : {y : Ordinal} → infinite-d y → Nat
+ω→nato : {y : Ordinal} → Omega-d y → Nat
 ω→nato iφ = Zero
 ω→nato (isuc lt) = Suc (ω→nato lt)
 
-ω→nat : (n : HOD) → infinite ∋ n → Nat
+ω→nat : (n : HOD) → Omega ∋ n → Nat
 ω→nat n = ω→nato
 
-ω∋nat→ω : {n : Nat} → def (od infinite) (& (nat→ω n))
-ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) (sym ord-od∅) iφ
-ω∋nat→ω {Suc n} = subst (λ k → def (od infinite) k) lemma (isuc ( ω∋nat→ω {n})) where
+ω∋nat→ω : {n : Nat} → def (od Omega) (& (nat→ω n))
+ω∋nat→ω {Zero} = subst (λ k → def (od Omega) k) (sym ord-od∅) iφ
+ω∋nat→ω {Suc n} = subst (λ k → def (od Omega) k) lemma (isuc ( ω∋nat→ω {n})) where
     lemma :  & (Union (* (& (nat→ω n)) , (* (& (nat→ω n)) , * (& (nat→ω n))))) ≡ & (nat→ω (Suc n))
     lemma = subst (λ k → & (Union (k , ( k , k ))) ≡ & (nat→ω (Suc n))) (sym *iso) refl
 
@@ -191,12 +191,12 @@
 ωs≠0 : (x : HOD) →  ¬ ( Union ( x , (x , x)) ≡ od∅ )
 ωs≠0 y eq =  ⊥-elim ( ¬x<0 (subst (λ k → & y  o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (& y )) eq (ω-∈s y) ))) )
 
-nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
-nat→ω-iso {i} = ε-induction {λ i →  (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i  } ind i where
-     ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) →
-                                            (lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x
+nat→ω-iso : {i : HOD} → (lt : Omega ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
+nat→ω-iso {i} = ε-induction {λ i →  (lt : Omega ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i  } ind i where
+     ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : Omega ∋ y) → nat→ω (ω→nat y lt) ≡ y) →
+                                            (lt : Omega ∋ x) → nat→ω (ω→nat x lt) ≡ x
      ind {x} prev lt = ind1 lt *iso where
-         ind1 : {ox : Ordinal } → (ltd : infinite-d ox ) → * ox ≡ x → nat→ω (ω→nato ltd) ≡ x
+         ind1 : {ox : Ordinal } → (ltd : Omega-d ox ) → * ox ≡ x → nat→ω (ω→nato ltd) ≡ x
          ind1 {o∅} iφ refl = sym o∅≡od∅
          ind1 (isuc {x₁} ltd) ox=x = begin
               nat→ω (ω→nato (isuc ltd) )
@@ -211,23 +211,23 @@
                lemma0 :  x ∋ * x₁
                lemma0 = subst (λ k → odef k (& (* x₁))) (trans (sym *iso) ox=x)
                    record { owner = & ( * x₁ , * x₁ ) ; ao = case2 refl ; ox = subst (λ k → odef k (& (* x₁))) (sym *iso) (case1 refl)  }
-               lemma1 : infinite ∋ * x₁
-               lemma1 = subst (λ k → odef infinite k) (sym &iso) ltd
-               lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1
+               lemma1 : Omega ∋ * x₁
+               lemma1 = subst (λ k → odef Omega k) (sym &iso) ltd
+               lemma3 : {x y : Ordinal} → (ltd : Omega-d x ) (ltd1 : Omega-d y ) → y ≡ x → ltd ≅ ltd1
                lemma3 iφ iφ refl = HE.refl
                lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso eq (c<→o< (ω-∈s (* y)) )))
                lemma3 (isuc {y} ltd)  iφ eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso (sym eq) (c<→o< (ω-∈s (* y)) )))
                lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (sym eq))
                ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅  (ω-prev-eq eq)) t
-               lemma2 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1
+               lemma2 : {x y : Ordinal} → (ltd : Omega-d x ) (ltd1 : Omega-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1
                lemma2 {x} {y} ltd ltd1 eq = lemma6 eq (lemma3 {x} {y} ltd ltd1 eq)  where
-                   lemma6 : {x y : Ordinal} → {ltd : infinite-d x } {ltd1 : infinite-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1
+                   lemma6 : {x y : Ordinal} → {ltd : Omega-d x } {ltd1 : Omega-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1
                    lemma6 refl HE.refl = refl
                lemma :  nat→ω (ω→nato ltd) ≡ * x₁
-               lemma = trans  (cong (λ k →  nat→ω  k) (lemma2 {x₁} {_} ltd (subst (λ k → infinite-d k ) (sym &iso) ltd)  &iso ) ) ( prev {* x₁} lemma0 lemma1 )
+               lemma = trans  (cong (λ k →  nat→ω  k) (lemma2 {x₁} {_} ltd (subst (λ k → Omega-d k ) (sym &iso) ltd)  &iso ) ) ( prev {* x₁} lemma0 lemma1 )
 
 
-ω→nat-iso0 : (x : Nat) → {ox : Ordinal } → (ltd : infinite-d ox) → * ox ≡ nat→ω x → ω→nato ltd ≡ x
+ω→nat-iso0 : (x : Nat) → {ox : Ordinal } → (ltd : Omega-d ox) → * ox ≡ nat→ω x → ω→nato ltd ≡ x
 ω→nat-iso0 Zero iφ eq = refl
 ω→nat-iso0 (Suc x) iφ eq = ⊥-elim ( ωs≠0 _ (trans (sym eq) o∅≡od∅ ))
 ω→nat-iso0 Zero (isuc ltd) eq = ⊥-elim ( ωs≠0 _ (subst (λ k → k ≡ od∅  ) *iso eq ))
--- a/src/OrdUtil.agda	Sat Jun 03 17:31:28 2023 +0900
+++ b/src/OrdUtil.agda	Sun Jun 04 16:58:39 2023 +0900
@@ -12,7 +12,7 @@
 
 open Ordinals.Ordinals  O
 open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
+-- open Ordinals.IsNext isNext
 
 o<-dom :   { x y : Ordinal } → x o< y → Ordinal
 o<-dom  {x} _ = x
@@ -253,11 +253,11 @@
   → ¬ p
 FExists  {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
 
-nexto∅ : {x : Ordinal} → o∅ o< next x
-nexto∅ {x} with trio< o∅ x
-nexto∅ {x} | tri< a ¬b ¬c = ordtrans a x<nx
-nexto∅ {x} | tri≈ ¬a b ¬c = subst (λ k → k o< next x) (sym b) x<nx
-nexto∅ {x} | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
+-- nexto∅ : {x : Ordinal} → o∅ o< next x
+-- nexto∅ {x} with trio< o∅ x
+-- nexto∅ {x} | tri< a ¬b ¬c = ordtrans a x<nx
+-- nexto∅ {x} | tri≈ ¬a b ¬c = subst (λ k → k o< next x) (sym b) x<nx
+-- nexto∅ {x} | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
 
 -- next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
 -- next< {x} {y} {z} x<nz y<nx with trio< y (next z)
@@ -283,13 +283,13 @@
 -- nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx<nx (ordtrans <-osuc x<nx) c
 --    (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
 
-next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y)
-next-is-limit {x} {y} eq = o<¬≡ (sym eq) (osuc<nx y<nx) where
-    y<nx : y o< next x
-    y<nx = osuc< (sym eq)
+-- next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y)
+-- next-is-limit {x} {y} eq = o<¬≡ (sym eq) (osuc<nx y<nx) where
+--     y<nx : y o< next x
+--     y<nx = osuc< (sym eq)
 
-omax<next : {x y : Ordinal} → x o< y → omax x y o< next y
-omax<next {x} {y} x<y = subst (λ k → k o< next y ) (omax< _ _ x<y ) (osuc<nx x<nx)
+-- omax<next : {x y : Ordinal} → x o< y → omax x y o< next y
+-- omax<next {x} {y} x<y = subst (λ k → k o< next y ) (omax< _ _ x<y ) (osuc<nx x<nx)
 
 -- x<ny→≡next : {x y : Ordinal} → x o< y → y o< next x → next x ≡ next y
 -- x<ny→≡next {x} {y} x<y y<nx with trio< (next x) (next y)
@@ -319,11 +319,11 @@
 -- omax<nomax {x} {y} | tri≈ ¬a refl ¬c = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx )
 -- omax<nomax {x} {y} | tri> ¬a ¬b c    = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx )
 
-omax<nx : {x y z : Ordinal} → x o< next z → y o< next z → omax x y o< next z
-omax<nx {x} {y} {z} x<nz y<nz with trio< x y
-omax<nx {x} {y} {z} x<nz y<nz | tri< a ¬b ¬c = osuc<nx y<nz
-omax<nx {x} {y} {z} x<nz y<nz | tri≈ ¬a refl ¬c = osuc<nx y<nz
-omax<nx {x} {y} {z} x<nz y<nz | tri> ¬a ¬b c = osuc<nx x<nz
+-- omax<nx : {x y z : Ordinal} → x o< next z → y o< next z → omax x y o< next z
+-- omax<nx {x} {y} {z} x<nz y<nz with trio< x y
+-- omax<nx {x} {y} {z} x<nz y<nz | tri< a ¬b ¬c = osuc<nx y<nz
+-- omax<nx {x} {y} {z} x<nz y<nz | tri≈ ¬a refl ¬c = osuc<nx y<nz
+-- omax<nx {x} {y} {z} x<nz y<nz | tri> ¬a ¬b c = osuc<nx x<nz
 
 -- nn<omax : {x nx ny : Ordinal} → x o< next nx → x o< next ny → x o< next (omax nx ny)
 -- nn<omax {x} {nx} {ny} xnx xny with trio< nx ny
--- a/src/Ordinals.agda	Sat Jun 03 17:31:28 2023 +0900
+++ b/src/Ordinals.agda	Sun Jun 04 16:58:39 2023 +0900
@@ -16,7 +16,7 @@
      oprev : ord
      oprev=x : osuc oprev ≡ x 
 
-record IsOrdinals {n : Level} (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
+record IsOrdinals {n : Level} (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n)  : Set (suc (suc n)) where
    field
      ordtrans : {x y z : ord }  → x o< y → y o< z → x o< z
      trio<    : Trichotomous {n} _≡_  _o<_ 
@@ -29,30 +29,18 @@
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
 
-
-record IsNext {n : Level } (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
-   field
-     x<nx :    { y : ord } → (y o< next y )
-     osuc<nx : { x y : ord } → x o< next y → osuc x o< next y 
-     --
-     -- this means we have some non constructive previous, it looks bad
-     -- ¬nx<nx :  {x y : ord} → y o< x → x o< next y →  ¬ ((z : ord) → ¬ (x ≡ osuc z)) 
-
 record Ordinals {n : Level} : Set (suc (suc n)) where
    field
      Ordinal : Set n
      o∅ : Ordinal
      osuc : Ordinal → Ordinal
      _o<_ : Ordinal → Ordinal → Set n
-     next :  Ordinal → Ordinal
-     isOrdinal : IsOrdinals Ordinal o∅ osuc _o<_ next
-     isNext : IsNext Ordinal o∅ osuc _o<_ next
+     isOrdinal : IsOrdinals Ordinal o∅ osuc _o<_ 
 
 module inOrdinal  {n : Level} (O : Ordinals {n} ) where
 
   open Ordinals  O
   open IsOrdinals isOrdinal
-  open IsNext isNext
 
   TransFinite0 : { ψ : Ordinal  → Set n }
           → ( (x : Ordinal)  → ( (y : Ordinal  ) → y o< x → ψ y ) → ψ x )
--- a/src/PFOD.agda	Sat Jun 03 17:31:28 2023 +0900
+++ b/src/PFOD.agda	Sun Jun 04 16:58:39 2023 +0900
@@ -27,7 +27,7 @@
 import ODUtil
 open Ordinals.Ordinals  O
 open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
+-- open Ordinals.IsNext isNext
 open OrdUtil O
 open ODUtil O
 
@@ -56,9 +56,7 @@
 data Hω2 :  (i : Nat) ( x : Ordinal  ) → Set n where
   hφ :  Hω2 0 o∅
   h0 : {i : Nat} {x : Ordinal  } → Hω2 i x  →
-    Hω2 (Suc i) (& (Union ((< nat→ω i , nat→ω 0 >) ,  * x )))
-  h1 : {i : Nat} {x : Ordinal  } → Hω2 i x  →
-    Hω2 (Suc i) (& (Union ((< nat→ω i , nat→ω 1 >) ,  * x )))
+    Hω2 (Suc i) (& (Union ((nat→ω i , nat→ω i) ,  * x )))
   he : {i : Nat} {x : Ordinal  } → Hω2 i x  →
     Hω2 (Suc i) x
 
@@ -69,42 +67,61 @@
 
 open Hω2r
 
+hw⊆POmega :  {y : Ordinal} → Hω2r y → odef (Power Omega) y
+hw⊆POmega {y} r = odmax1 (Hω2r.count r) (Hω2r.hω2 r) where
+    odmax1 : {y : Ordinal} (i : Nat)  →  Hω2 i y → odef (Power Omega) y
+    odmax1 0 hφ z xz = ⊥-elim ( ¬x<0 (subst (λ k → odef k z) o∅≡od∅  xz ))
+    odmax1 (Suc i) (h0 {_} {y} hw) = pf01 where
+        pf00 : odef ( Power Omega) y
+        pf00 = odmax1 i hw
+        pf01 : odef (Power Omega) (& (Union ((nat→ω i , nat→ω i ) , * y)))
+        pf01 z xz with subst (λ k → odef k z ) *iso xz
+        ... | record { owner = owner ; ao = case1 refl ; ox = ox } = pf02 where
+             pf02 : Omega-d z
+             pf02 with subst (λ k → odef k z) *iso ox
+             ... | case1 refl = ω∋nat→ω {i}
+             ... | case2 refl = ω∋nat→ω {i}
+        ... | record { owner = owner ; ao = case2 refl ; ox = ox } = pf00 _ (subst (λ k → odef k z) *iso ox)
+    odmax1 (Suc i) (he {_} {y} hw) = pf00 where
+        pf00 : odef ( Power Omega) y
+        pf00 = odmax1 i hw
+
+--
+-- Set of limited partial function of Omega
+--
 HODω2 :  HOD
-HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where
-    P  : (i j : Nat) (x : Ordinal ) → HOD
-    P  i j x = ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) , * x
-    -- nat1 : (i : Nat) (x : Ordinal) → & (nat→ω i) o< next x
-    -- nat1 i x =  next< nexto∅ ( <odmax infinite (ω∋nat→ω {i}))
-    lemma1 : (i j : Nat) (x : Ordinal ) → osuc (& (P i j x)) o< next x
-    lemma1 i j x = ? -- osuc<nx (pair-<xy (pair-<xy (pair-<xy (nat1 i x) (nat1 i x) ) (pair-<xy (nat1 i x) (nat1 j x) ) )
-    --      (subst (λ k → k o< next x) (sym &iso) x<nx ))
-    lemma : (i j : Nat) (x : Ordinal ) → & (Union (P i j x)) o< next x
-    lemma i j x = ? -- next< (lemma1 i j x ) ho<
-    odmax0 :  {y : Ordinal} → Hω2r y → y o< next o∅ 
-    odmax0 {y} r with hω2 r
-    ... | hφ = x<nx
-    ... | h0 {i} {x} t = ? -- jnext< (odmax0 record { count = i ; hω2 = t }) (lemma i 0 x)
-    ... | h1 {i} {x} t = ? -- jnext< (odmax0 record { count = i ; hω2 = t }) (lemma i 1 x)
-    ... | he {i} {x} t = ? -- jnext< (odmax0 record { count = i ; hω2 = t }) x<nx
+HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = & (Power Omega)
+  ; <odmax = λ lt → odef< (hw⊆POmega  lt) } 
+
+HODω2⊆Omega : {x : HOD} → HODω2 ∋ x → x ⊆ Omega 
+HODω2⊆Omega {x} hx {z} wz = hw⊆POmega hx _ (subst (λ k → odef k z) (sym *iso) wz)
+
+record HwStep : Set n where
+   field 
+     x : Ordinal
+     i : Nat
+     isHw : Hω2 i x
 
-3→Hω2 : List (Maybe Two) → HOD
-3→Hω2 t = list→hod t 0 where
-   list→hod : List (Maybe Two) → Nat → HOD
-   list→hod [] _ = od∅
-   list→hod (just i0 ∷ t) i = Union (< nat→ω i , nat→ω 0 > , ( list→hod t (Suc i) )) 
-   list→hod (just i1 ∷ t) i = Union (< nat→ω i , nat→ω 1 > , ( list→hod t (Suc i) )) 
-   list→hod (nothing ∷ t) i = list→hod t (Suc i ) 
+3→Hω2 : List Two → HOD
+3→Hω2 t = * (HwStep.x (list→hod t))  where
+   list→hod : List Two → HwStep
+   list→hod []  = record { x = o∅ ; i = 0 ; isHw = hφ }
+   list→hod (i0 ∷ t)  = record { x = & (Union ( (nat→ω (HwStep.i pf01) , nat→ω (HwStep.i pf01))  , * x )) 
+            ; i = Suc (HwStep.i pf01) ; isHw = h0 (HwStep.isHw pf01) } where 
+        pf01 : HwStep
+        pf01 = list→hod t 
+        x = HwStep.x pf01
+   list→hod (i1 ∷ t)  = list→hod t 
 
-Hω2→3 : (x :  HOD) → HODω2 ∋ x → List (Maybe Two) 
+Hω2→3 : (x :  HOD) → HODω2 ∋ x → List Two 
 Hω2→3 x = lemma where
-   lemma : { y : Ordinal } →  Hω2r y → List (Maybe Two)
+   lemma : { y : Ordinal } →  Hω2r y → List Two
    lemma record { count = 0 ; hω2 = hφ } = []
-   lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = just i0 ∷ lemma record { count = i ; hω2 =  hω3 }
-   lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = just i1 ∷ lemma record { count = i ; hω2 =  hω3 }
-   lemma record { count = (Suc i) ; hω2 = (he hω3) } = nothing ∷ lemma record { count = i ; hω2 =  hω3 }
+   lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = i0 ∷ lemma record { count = i ; hω2 =  hω3 }
+   lemma record { count = (Suc i) ; hω2 = (he hω3) } = i1 ∷ lemma record { count = i ; hω2 =  hω3 }
 
 ω→2 : HOD
-ω→2 = Power infinite
+ω→2 = Power Omega
 
 ω2→f : (x : HOD) → ω→2 ∋ x → Nat → Two
 ω2→f x lt n with ODC.∋-p O x (nat→ω n)
@@ -112,10 +129,10 @@
 ω2→f x lt n | no ¬p = i0
 
 fω→2-sel : ( f : Nat → Two ) (x : HOD) → Set n
-fω→2-sel f x = (infinite ∋ x) ∧ ( (lt : odef infinite (&  x) ) → f (ω→nat x lt) ≡ i1 )
+fω→2-sel f x = (Omega ∋ x) ∧ ( (lt : odef Omega (&  x) ) → f (ω→nat x lt) ≡ i1 )
 
 fω→2 : (Nat → Two) → HOD
-fω→2 f = Select infinite (fω→2-sel f)
+fω→2 f = Select Omega (fω→2-sel f)
 
 open _==_
 
@@ -123,9 +140,9 @@
 postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
 
 ω2∋f : (f : Nat → Two) → ω→2 ∋ fω→2 f
-ω2∋f f = power← infinite (fω→2 f) (λ {x} lt →  proj1 ((proj2 (selection {fω→2-sel f} {infinite} )) lt))
+ω2∋f f = power← Omega (fω→2 f) (λ {x} lt →  proj1 ((proj2 (selection {fω→2-sel f} {Omega} )) lt))
 
-ω→2f≡i1 : (X i : HOD) → (iω : infinite ∋ i) → (lt : ω→2 ∋ X ) → ω2→f X lt (ω→nat i iω)  ≡ i1 → X ∋ i
+ω→2f≡i1 : (X i : HOD) → (iω : Omega ∋ i) → (lt : ω→2 ∋ X ) → ω2→f X lt (ω→nat i iω)  ≡ i1 → X ∋ i
 ω→2f≡i1 X i iω lt eq with ODC.∋-p O X (nat→ω (ω→nat i iω))
 ω→2f≡i1 X i iω lt eq | yes p = subst (λ k → X ∋ k ) (nat→ω-iso iω) p
 
@@ -133,10 +150,10 @@
 eq→ (ω2→f-iso X lt) {x} ⟪ ωx , ⟪ ωx1 , iso ⟫ ⟫ = le00 where
     le00 : odef X x
     le00 = subst (λ k → odef X k) &iso ( ω→2f≡i1 _ _ ωx1 lt  (iso ωx1)  )
-eq← (ω2→f-iso X lt) {x} Xx = ⟪ subst (λ k → odef infinite k) &iso le02  , ⟪ le02 , le01 ⟫ ⟫ where
-    le02 : infinite ∋ * x
-    le02 = power→ infinite _ lt (subst (λ k → odef X k) (sym &iso) Xx) 
-    le01 : (wx : odef infinite (& (* x))) → ω2→f X lt (ω→nat (* x) wx) ≡ i1
+eq← (ω2→f-iso X lt) {x} Xx = ⟪ subst (λ k → odef Omega k) &iso le02  , ⟪ le02 , le01 ⟫ ⟫ where
+    le02 : Omega ∋ * x
+    le02 = power→ Omega _ lt (subst (λ k → odef X k) (sym &iso) Xx) 
+    le01 : (wx : odef Omega (& (* x))) → ω2→f X lt (ω→nat (* x) wx) ≡ i1
     le01 wx   with ODC.∋-p O X (nat→ω (ω→nat _ wx) )
     ... | yes p  = refl
     ... | no ¬p  = ⊥-elim ( ¬p (subst (λ k → odef X k ) le03 Xx )) where
@@ -148,11 +165,11 @@
     le01 : (x : Nat) → ω2→f (fω→2 f) (ω2∋f f) x ≡ f x
     le01 x with  ODC.∋-p O (fω→2 f) (nat→ω x) 
     le01 x | yes p = subst (λ k → i1 ≡ f k ) (ω→nat-iso0 x (proj1 (proj2 p)) (trans *iso *iso)) (sym ((proj2 (proj2 p)) le02)) where
-        le02 :  infinite-d (& (* (& (nat→ω x))))
+        le02 :  Omega-d (& (* (& (nat→ω x))))
         le02 = proj1 (proj2 p )
     le01 x | no ¬p = sym ( ¬i1→i0 le04 ) where
         le04 : ¬ f x ≡ i1
-        le04 fx=1 = ¬p ⟪ ω∋nat→ω {x} , ⟪ subst (λ k → infinite-d k) (sym &iso) (ω∋nat→ω {x})  , le05 ⟫ ⟫ where
-            le05 : (lt : infinite-d (& (* (& (nat→ω x))))) → f (ω→nato lt) ≡ i1
+        le04 fx=1 = ¬p ⟪ ω∋nat→ω {x} , ⟪ subst (λ k → Omega-d k) (sym &iso) (ω∋nat→ω {x})  , le05 ⟫ ⟫ where
+            le05 : (lt : Omega-d (& (* (& (nat→ω x))))) → f (ω→nato lt) ≡ i1
             le05 lt = trans (cong f (ω→nat-iso0 x lt (trans *iso *iso))) fx=1
 
--- a/src/Topology.agda	Sat Jun 03 17:31:28 2023 +0900
+++ b/src/Topology.agda	Sun Jun 04 16:58:39 2023 +0900
@@ -25,7 +25,7 @@
 import ODUtil
 open Ordinals.Ordinals  O
 open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
+-- open Ordinals.IsNext isNext
 open OrdUtil O
 open ODUtil O
 
--- a/src/Tychonoff.agda	Sat Jun 03 17:31:28 2023 +0900
+++ b/src/Tychonoff.agda	Sun Jun 04 16:58:39 2023 +0900
@@ -24,7 +24,7 @@
 import ODUtil
 open Ordinals.Ordinals  O
 open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
+-- open Ordinals.IsNext isNext
 open OrdUtil O
 open ODUtil O
 
--- a/src/VL.agda	Sat Jun 03 17:31:28 2023 +0900
+++ b/src/VL.agda	Sun Jun 04 16:58:39 2023 +0900
@@ -18,7 +18,7 @@
 import ODUtil
 open Ordinals.Ordinals  O
 open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
+--  open Ordinals.IsNext isNext
 open OrdUtil O
 open ODUtil O
 
--- a/src/ZProduct.agda	Sat Jun 03 17:31:28 2023 +0900
+++ b/src/ZProduct.agda	Sun Jun 04 16:58:39 2023 +0900
@@ -24,7 +24,7 @@
 
 open Ordinals.Ordinals  O
 open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
+-- open Ordinals.IsNext isNext
 open OrdUtil O
 open ODUtil O
 
@@ -352,6 +352,12 @@
        lemma4 : ZFProduct A B (& < * z , * (Func.func F (subst (λ k → odef A k) (sym &iso) az)) > )
        lemma4 = ab-pair az (Func.is-func F (subst (λ k → odef A k) (sym &iso) az))
 
+TwoHOD : HOD
+TwoHOD = ( od∅ , ( od∅ ,  od∅ ))
+
+Aleph1 : HOD
+Aleph1 = Funcs Omega TwoHOD
+
 record Injection (A B : Ordinal ) : Set n where
    field
        i→  : (x : Ordinal ) → odef (* A)  x → Ordinal
--- a/src/cardinal.agda	Sat Jun 03 17:31:28 2023 +0900
+++ b/src/cardinal.agda	Sun Jun 04 16:58:39 2023 +0900
@@ -27,7 +27,7 @@
 import ODUtil
 open Ordinals.Ordinals  O
 open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
+-- open Ordinals.IsNext isNext
 open OrdUtil O
 open ODUtil O
 
--- a/src/filter-util.agda	Sat Jun 03 17:31:28 2023 +0900
+++ b/src/filter-util.agda	Sun Jun 04 16:58:39 2023 +0900
@@ -24,7 +24,7 @@
 import ODUtil
 open Ordinals.Ordinals  O
 open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
+-- open Ordinals.IsNext isNext
 open OrdUtil O
 open ODUtil O
 
--- a/src/filter.agda	Sat Jun 03 17:31:28 2023 +0900
+++ b/src/filter.agda	Sun Jun 04 16:58:39 2023 +0900
@@ -24,7 +24,7 @@
 import ODUtil
 open Ordinals.Ordinals  O
 open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
+-- open Ordinals.IsNext isNext
 open OrdUtil O
 open ODUtil O
 
--- a/src/generic-filter.agda	Sat Jun 03 17:31:28 2023 +0900
+++ b/src/generic-filter.agda	Sun Jun 04 16:58:39 2023 +0900
@@ -25,7 +25,7 @@
 import ODUtil
 open Ordinals.Ordinals  O
 open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
+-- open Ordinals.IsNext isNext
 open OrdUtil O
 open ODUtil O
 
--- a/src/maximum-filter.agda	Sat Jun 03 17:31:28 2023 +0900
+++ b/src/maximum-filter.agda	Sun Jun 04 16:58:39 2023 +0900
@@ -24,7 +24,7 @@
 import ODUtil
 open Ordinals.Ordinals  O
 open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
+-- open Ordinals.IsNext isNext
 open OrdUtil O
 open ODUtil O
 
--- a/src/ordinal.agda	Sat Jun 03 17:31:28 2023 +0900
+++ b/src/ordinal.agda	Sun Jun 04 16:58:39 2023 +0900
@@ -236,7 +236,6 @@
    ; o∅ = o∅
    ; osuc = osuc
    ; _o<_ = _o<_
-   ; next = next
    ; isOrdinal = record {
        ordtrans = ordtrans
      ; trio< = trio<
@@ -246,12 +245,12 @@
      ; TransFinite = TransFinite2
      ; o<-irr = OrdIrr
      ; Oprev-p  = Oprev-p 
-   } ;
-   isNext = record {
-        x<nx = x<nx 
-      ; osuc<nx = λ {x} {y} → osuc<nx {x} {y}
-      -- ; ¬nx<nx = ¬nx<nx 
-   }
+   } --
+   -- isNext = record {
+   --     x<nx = x<nx 
+   --   ; osuc<nx = λ {x} {y} → osuc<nx {x} {y}
+   --   -- ; ¬nx<nx = ¬nx<nx 
+   -- }
   } where
      next : Ordinal {suc n} → Ordinal {suc n}
      next (ordinal lv ord) = ordinal (Suc lv) (Φ (Suc lv))
--- a/src/zorn.agda	Sat Jun 03 17:31:28 2023 +0900
+++ b/src/zorn.agda	Sun Jun 04 16:58:39 2023 +0900
@@ -32,7 +32,7 @@
 import ODUtil
 open Ordinals.Ordinals  O
 open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
+-- open Ordinals.IsNext isNext
 open OrdUtil O
 open ODUtil O