--- a/LEMC.agda	Sun Jul 19 10:02:43 2020 +0900
+++ b/LEMC.agda	Sun Jul 19 12:26:17 2020 +0900
@@ -40,12 +40,12 @@
     ; _∋_ = _∋_ 
     ; _≈_ = _=h=_ 
     ; ∅  = od∅
-    ; Select = ?
+    ; Select = {!!}
     ; isZFC = isZFC
  } where
     -- infixr  200 _∈_
     -- infixr  230 _∩_ _∪_
-    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ ?
+    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ {!!}
     isZFC = record {
        choice-func = λ A {X} not A∋X → a-choice (choice-func X not );
        choice = λ A {X} A∋X not → is-in (choice-func X not)

--- a/ODC.agda	Sun Jul 19 10:02:43 2020 +0900
+++ b/ODC.agda	Sun Jul 19 12:26:17 2020 +0900
@@ -69,6 +69,11 @@
 decp  p | case1 x = yes x
 decp  p | case2 x = no x
 
+∋-p : (A x : HOD ) → Dec ( A ∋ x ) 
+∋-p A x with p∨¬p ( A ∋ x ) -- LEM
+∋-p A x | case1 t  = yes t
+∋-p A x | case2 t  = no (λ x → t x)
+
 double-neg-eilm : {A : Set n} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
 double-neg-eilm  {A} notnot with decp  A                         -- assuming axiom of choice
 ... | yes p = p

--- 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 {