--- a/filter.agda	Wed Jul 22 08:08:04 2020 +0900
+++ b/filter.agda	Thu Jul 23 17:50:28 2020 +0900
@@ -405,7 +405,7 @@
 record 3Gf (f : Nat → Two) (p : List Three ) : Set where
    field
      3gn  : Nat
-     3f<n : (f 3↑ 3gn) 3⊆ p
+     3f<n : p 3⊆ (f 3↑ 3gn)
 
 open 3Gf
 
@@ -421,12 +421,9 @@
      ; filter2 = λ {p} {q} fp fq  → record { 3gn = min (3gn fp) (3gn fq) ; 3f<n = lemma2 p q fp fq }
  }  where
       lemma1 : (p q : List Three ) → (fp : 3Gf f p) →  (p⊆q : p 3⊆ q) → 3Gf f q
-      lemma1 p q fp p⊆q  = record { 3gn = 3gn fp  ; 3f<n = 3⊆trans {f 3↑ 3gn fp } {p} {q} (3f<n fp) p⊆q }
-      lemma2 : (p q : List Three ) → (fp : 3Gf f p) → (fq : 3Gf f q)  → (f 3↑ min (3gn fp) (3gn fq)) 3⊆ (p 3∩ q)
-      lemma2 p q fp fq = 3⊆∩f {f 3↑ min (3gn fp) (3gn fq) } {p} {q} (3⊆trans {bb} {f 3↑ (3gn fp)} {p} (3↑< {_} {bm} (m⊓n≤m _ _ )) (3f<n fp))
-                                                                    (3⊆trans {bb} {f 3↑ (3gn fq)} {q} (3↑< {_} {bm} (m⊓n≤n _ _ )) (3f<n fq))  where
-             bb = f 3↑ min (3gn fp) (3gn fq)
-             bm =  min (3gn fp) (3gn fq)
+      lemma1 p q fp p⊆q  = record { 3gn = 3gn fp  ; 3f<n = {!!} }
+      lemma2 : (p q : List Three ) → (fp : 3Gf f p) → (fq : 3Gf f q)  → (p 3∩ q) 3⊆ (f 3↑ min (3gn fp) (3gn fq))
+      lemma2 p q fp fq = {!!}
 
 record _f⊆_ {n : Level } (f g : PFunc {n} ) : Set (suc n) where
   field
@@ -617,3 +614,30 @@
 Hω2f→Hω2 p = {!!} -- record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} }
 
 
+record CountableOrdinal : Set (suc (suc n)) where
+   field
+       ctl→ : Nat → Ordinal
+       ctl← : Ordinal → Nat
+       ctl-iso→ : { x : Ordinal } → ctl→ (ctl← x ) ≡ x 
+       ctl-iso← : { x : Nat }  → ctl← (ctl→ x ) ≡ x
+       
+record GenericFilter (P : HOD) : Set (suc n) where
+    field
+       genf : Filter P
+       generic : (D : Dense P ) → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ )
+
+record F-GenericFilter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L  → L → Set n)  (_∩_ : L → L → L ) : Set (suc n) where
+    field
+       GFilter : F-Filter L PL _⊆_ _∩_
+       Intersection : (D : F-Dense L PL _⊆_ _∩_ ) → { x : L } → F-Dense.dense D x →  L
+       Generic : (D : F-Dense L PL _⊆_ _∩_ ) → { x : L } → ( y : F-Dense.dense D x) →  F-Filter.filter GFilter (Intersection D y )
+
+data PD (P : HOD) (C : CountableOrdinal) : (x : Ordinal) (n : Nat) →  Set (suc n) where
+    pd0 : (p : Ordinal ) → odef (ord→od P) p → PD C p 0 
+    pdq : {q pnx : Ordinal } {n : Nat}  → (pn : PD P C pnx n ) → odef (ctl→ C n) q → ord→od p0x ⊆ ord→od q → PD P C q (suc n) 
+
+P-GenericFilter : {P : HOD} → (C : CountableOrdinal) → GenericFilter P
+P-GenericFilter {P} C = record {
+      genf = record { filter = {!!} ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} }
+    ; generic = λ D → {!!}
+   }