--- a/filter.agda	Sun Jul 19 10:02:43 2020 +0900
+++ b/filter.agda	Sun Jul 19 12:26:17 2020 +0900
@@ -152,6 +152,37 @@
 import OPair
 open OPair O
 
+data Two : Set n where
+   i0 : Two
+   i1 : Two
+
+record PFunc : Set (suc n) where
+   field
+      restrict : Nat → Set n
+      map : (x : Nat ) → restrict x → Two
+
+open PFunc
+
+record _f⊆_ (f g : PFunc) : Set (suc n) where
+  field
+     feq : (x : Nat) → (fr : restrict f x ) →  (gr : restrict g x ) → map f x fr ≡ map g x gr
+
+full-func  : Set n
+full-func = Nat → Two
+
+full→PF : (Nat → Two) → PFunc
+full→PF f = record { restrict = λ x → One ; map = λ x _ → f x }
+
+_↑_ : (Nat → Two) → Nat → PFunc
+f ↑ i = record { restrict = λ x → Lift n (x ≤ i) ; map = λ x _ → f x }
+
+record F-Filter (PL : Set n) (L : PL ) ( _⊆_ : PL → PL → Set n) ( _∋_ : PL → PL → Set n) : Set (suc n) where
+   field
+       filter : PL
+       f⊆PL :  filter ⊆ L
+       filter1 : { p q : PL } →  q ⊆ L  → filter ∋ p →  p ⊆ q  → filter ∋ q
+       filter2 : { p q : PL } → filter ∋ p →  filter ∋ q  → (filter ∋ p) ∧ (filter ∋ q)
+
 ODSuc : (y : HOD) → infinite ∋ y → HOD
 ODSuc y lt = Union (y , (y , y)) 
 
@@ -184,17 +215,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
 
-data Two : Set n where
-   i0 : Two
-   i1 : Two
+ω→2 : HOD
+ω→2 = Replace (Power infinite) (λ p p⊆i → Replace infinite (λ x i∋x → < x , repl p x > )) where
+  repl : HOD → HOD → HOD
+  repl p x with ODC.∋-p O p x
+  ... | yes _  = nat→ω 1
+  ... | no _  = nat→ω 0
 
-record ω2r : Set n where
-   field
-     func2 : Nat → Two
-     ω2 : {!!}
-
-ω→2 : HOD
-ω→2 = Replace infinite (λ x → < x , {!!} > )
+record _↑n (f : HOD) (ω→2∋f : ω→2 ∋ f ) : Set n where
+   -- field
+      -- n : HOD
+      -- ? : Select f (λ x f∋x → ω→nat (π1 f∋x) < ω→nat n
+  
+Gf : {f : HOD} → ω→2 ∋ f  → HOD
+Gf {f} lt = Select HODω2 (λ x H∋x → {!!}   )
 
 G : (Nat → Two) → Filter HODω2
 G f = record {