--- a/filter.agda	Mon Jun 15 18:15:48 2020 +0900
+++ b/filter.agda	Tue Jun 23 15:12:43 2020 +0900
@@ -119,28 +119,17 @@
         lemma : (p : OD) → p ⊆ L   →  filter P ∋ (p ∪ (L ＼ p))
         lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L
 
-generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
-generated-filter {L} P p = {!!}
-
 record Dense  (P : OD ) : Set (suc n) where
    field
        dense : OD
        incl :  dense ⊆ P 
        dense-f : OD → OD
-       dense-p :  { p : OD} → P ∋ p  → p ⊆ (dense-f p) 
-
--- H(ω,2) = Power ( Power ω ) = Def ( Def ω))
-
-infinite = ZF.infinite OD→ZF
+       dense-d :  { p : OD} → P ∋ p  → dense ∋ dense-f p  
+       dense-p :  { p : OD} → P ∋ p  →  p ⊆ (dense-f p) 
 
-module in-countable-ordinal {n : Level} where
-
-   import ordinal
-
-   -- open  ordinal.C-Ordinal-with-choice 
-
-   Hω2 : Filter (Power (Power infinite))
-   Hω2 = {!!}
+--    the set of finite partial functions from ω to 2
+--
+-- Hω2 : Filter (Power (Power infinite))
 
 
 record Ideal  ( L : OD  ) : Set (suc n) where