--- a/filter.agda	Sun Jul 19 00:26:55 2020 +0900
+++ b/filter.agda	Sun Jul 19 03:24:39 2020 +0900
@@ -124,10 +124,10 @@
 record Dense  (P : HOD ) : Set (suc n) where
    field
        dense : HOD
-       incl :  dense ⊆ P 
+       incl :  dense ⊆ Power P 
        dense-f : HOD → HOD
-       dense-d :  { p : HOD} → P ∋ p  → dense ∋ dense-f p  
-       dense-p :  { p : HOD} → P ∋ p  →  p ⊆ (dense-f p) 
+       dense-d :  { p : HOD} → p ⊆ P → dense ∋ dense-f p  
+       dense-p :  { p : HOD} → p ⊆ P → p ⊆ (dense-f p) 
 
 record Ideal  ( L : HOD  ) : Set (suc n) where
    field
@@ -184,8 +184,20 @@
     ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {1} {x})
     ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx
 
-HODω2-Filter : Filter HODω2
-HODω2-Filter = record {
+data Two : Set n where
+   i0 : Two
+   i1 : Two
+
+record ω2r : Set n where
+   field
+     func2 : Nat → Two
+     ω2 : {!!}
+
+ω→2 : HOD
+ω→2 = Replace infinite (λ x → < x , {!!} > )
+
+G : (Nat → Two) → Filter HODω2
+G f = record {
        filter = {!!}
      ; f⊆PL = {!!}
      ; filter1 = {!!}
@@ -202,10 +214,6 @@
 
 -- the set of finite partial functions from ω to 2
 
-data Two : Set n where
-   i0 : Two
-   i1 : Two
-
 Hω2f : Set (suc n)
 Hω2f = (Nat → Set n) → Two