--- 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