--- a/filter.agda	Sat Jul 18 11:38:33 2020 +0900
+++ b/filter.agda	Sat Jul 18 12:29:38 2020 +0900
@@ -71,8 +71,6 @@
 q∩q⊆q = record { incl = λ lt → proj1 lt } 
 
 open HOD
-_=h=_ : (x y : HOD) → Set n
-x =h= y  = od x == od y
 
 -----
 --
@@ -157,16 +155,9 @@
 ODSuc : (y : HOD) → infinite ∋ y → HOD
 ODSuc y lt = Union (y , (y , y)) 
 
-nat→ω : Nat → HOD
-nat→ω Zero = od∅
-nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) 
+postulate  
+   ho< : {x : HOD} → hod-ord< {x} -- : ({x : HOD} → od→ord x o< next (odmax x)) 
 
-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∅
@@ -179,6 +170,8 @@
 
 HODω2 :  HOD
 HODω2 = record { od = record { def = λ x → Hω2 x } ; odmax = next o∅ ; <odmax = odmax0 } where
+    ω<next : {y : Ordinal} → infinite-d y → y o< next o∅
+    ω<next = ω<next-o∅ ho<
     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∅
@@ -187,6 +180,22 @@
     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} )))
 
+HODω2-Filter : Filter HODω2
+HODω2-Filter = record {
+       filter = {!!}
+     ; f⊆PL = {!!}
+     ; filter1 = {!!}
+     ; filter2 = {!!}
+   } where
+       filter0 : HOD   
+       filter0 = {!!}
+       f⊆PL1 :  filter0 ⊆ Power HODω2 
+       f⊆PL1 = {!!}
+       filter11 : { p q : HOD } →  q ⊆ HODω2  → filter0 ∋ p →  p ⊆ q  → filter0 ∋ q
+       filter11 = {!!}
+       filter12 : { p q : HOD } → filter0 ∋ p →  filter0 ∋ q  → filter0 ∋ (p ∩ q)
+       filter12 = {!!}
+
 -- the set of finite partial functions from ω to 2
 
 data Two : Set n where