# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595039913 -32400
# Node ID 67580311cc8e90a0178d7f47d67c1a1408b4fd46
# Parent  aad9249d1e8ff9c7572e7268636711489cdd227b
...

diff -r aad9249d1e8f -r 67580311cc8e OD.agda
--- a/OD.agda	Sat Jul 18 10:36:32 2020 +0900
+++ b/OD.agda	Sat Jul 18 11:38:33 2020 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-} 
 open import Level
 open import Ordinals
 module OD {n : Level } (O : Ordinals {n} ) where
@@ -400,27 +401,24 @@
     infinite' ho< = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
         u : (y : Ordinal ) → HOD
         u y = Union (ord→od y , (ord→od y , ord→od y))
+        --   next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
+        lemma8 : {y : Ordinal} → 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 
+        lemmaa : {x y : HOD} → od→ord x o< od→ord y → od→ord (x , y) o< next (od→ord y)
+        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 : {y : Ordinal} → od→ord (ord→od y , ord→od y) o< next (od→ord (ord→od y))
+        lemma81 {y} = nexto=n (subst (λ k →  od→ord (ord→od y , ord→od y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
+        lemma9 : {y : Ordinal} → 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 : {y : Ordinal} → od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y))
+        lemma71 = next< lemma81 lemma9
+        lemma1 : {y : Ordinal} → od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y))))
+        lemma1 = ho<
+        --- main recursion
         lemma : {y : Ordinal} → infinite-d y → y o< next o∅
         lemma {o∅} iφ = x<nx
-        lemma (isuc {y} x) = lemma2 where
-            --   next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
-            lemma0 : y o< next o∅
-            lemma0 = lemma x
-            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 
-            lemmaa : {x y : HOD} → od→ord x o< od→ord y → od→ord (x , y) o< next (od→ord y)
-            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)
-            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))
-            lemma71 = next< lemma81 lemma9
-            lemma1 : od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y))))
-            lemma1 = ho<
-            lemma2 : od→ord (u y) o< next o∅
-            lemma2 = next< lemma0 (next< (subst (λ k → od→ord (ord→od y , (ord→od y , ord→od y)) o< next k) diso lemma71 ) (nexto=n lemma1))
+        lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → od→ord (ord→od y , (ord→od y , ord→od y)) o< next k) diso lemma71 ) (nexto=n lemma1))
 
     nat→ω : Nat → HOD
     nat→ω Zero = od∅
@@ -432,6 +430,10 @@
         lemma iφ = Zero
         lemma (isuc lt) = Suc (lemma lt)
 
+    ω∋nat→ω : {n : Nat} → def (od infinite) (od→ord (nat→ω n))
+    ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) {!!} iφ
+    ω∋nat→ω {Suc n} = subst (λ k → def (od infinite) k) {!!} (isuc ( ω∋nat→ω {n}))
+
     _=h=_ : (x y : HOD) → Set n
     x =h= y  = od x == od y
 
diff -r aad9249d1e8f -r 67580311cc8e filter.agda
--- a/filter.agda	Sat Jul 18 10:36:32 2020 +0900
+++ b/filter.agda	Sat Jul 18 11:38:33 2020 +0900
@@ -146,12 +146,10 @@
 prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n
 prime-ideal {L} P {p} {q} =  ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )
 
+-------
 --    the set of finite partial functions from ω to 2
 --
---   ph2 : Nat → Set → 2
---   ph2 : Nat → Maybe 2
 --
--- Hω2 : Filter (Power (Power infinite))
 
 import OPair
 open OPair O
@@ -163,6 +161,13 @@
 nat→ω Zero = od∅
 nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) 
 
+postulate  -- we have proved in other module
+   ω∋nat→ω : {n : Nat} → def (od infinite) (od→ord (nat→ω n))
+   ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅
+
+postulate
+   ho< : {x : HOD} → hod-ord< {x} -- : ({x : HOD} → od→ord x o< next (odmax x)) 
+
 data Hω2 : ( x : Ordinal  ) → Set n where
   hφ :  Hω2 o∅
   h0 : {x : Ordinal  } → Hω2 x  →
@@ -173,7 +178,14 @@
     Hω2 (od→ord < nat→ω 2 , ord→od x >)
 
 HODω2 :  HOD
-HODω2 = record { od = record { def = λ x → Hω2 x } ; odmax = {!!} ; <odmax = {!!} }
+HODω2 = record { od = record { def = λ x → Hω2 x } ; odmax = next o∅ ; <odmax = odmax0 } where
+    lemma0 : {n y : Ordinal} → Hω2 y → odef infinite n  → od→ord < ord→od n , ord→od y > o< next y
+    lemma0 {n} {y} hw2 inf = nexto=n {!!} 
+    odmax0 : {y : Ordinal} → Hω2 y → y o< next o∅
+    odmax0 {o∅} hφ = x<nx
+    odmax0 (h0 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k →  od→ord < k , ord→od y >) oiso )  (lemma0 lt (ω∋nat→ω {0} )))
+    odmax0 (h1 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k →  od→ord < k , ord→od y >) oiso )  (lemma0 lt (ω∋nat→ω {1} )))
+    odmax0 (h2 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k →  od→ord < k , ord→od y >) oiso )  (lemma0 lt (ω∋nat→ω {2} )))
 
 -- the set of finite partial functions from ω to 2