--- a/OD.agda	Sun Jul 26 21:39:27 2020 +0900
+++ b/OD.agda	Mon Jul 27 09:29:41 2020 +0900
@@ -495,6 +495,9 @@
   ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
   }
 
+selection-in-domain : {ψ : HOD → Set n} {X y : HOD} → Select X ψ ∋ y → X ∋ y 
+selection-in-domain {ψ} {X} {y} lt = proj1 ((proj2 (selection {ψ} {X} )) lt)
+
 sup-c< :  (ψ : HOD → HOD) → {X x : HOD} → X ∋ x  → od→ord (ψ x) o< (sup-o X (λ y X∋y → od→ord (ψ (ord→od y))))
 sup-c< ψ {X} {x} lt = subst (λ k → od→ord (ψ k) o< _ ) oiso (sup-o< X lt )
 replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x

--- a/generic-filter.agda	Sun Jul 26 21:39:27 2020 +0900
+++ b/generic-filter.agda	Mon Jul 27 09:29:41 2020 +0900
@@ -124,6 +124,35 @@
 ω→2f x lt n | yes p = i1
 ω→2f x lt n | no ¬p = i0
 
+fω→2-sel : ( f : Nat → Two ) (x : HOD) → Set n
+fω→2-sel f x = (infinite ∋ x) ∧ ( (lt : odef infinite (od→ord  x) ) → f (ω→nat x lt) ≡ i1 )
+
+fω→2 : (Nat → Two) → HOD
+fω→2 f = Select infinite (fω→2-sel f)
+
+open _==_
+
+postulate f-extensionality : { n m : Level}  → Relation.Binary.PropositionalEquality.Extensionality n m
+
+ω2f : (f : Nat → Two) → ω→2 ∋ fω→2 f
+ω2f f = power← infinite (fω→2 f) (λ {x} lt →  proj1 ((proj2 (selection {fω→2-sel f} {infinite} )) lt))
+ 
+ω→2f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω→2f X lt )  =h= X
+ω→2f-iso X lt = record {
+     eq→ = eq1
+   ; eq← = eq2
+  } where
+     eq1 : {x : Ordinal} → odef (fω→2 (ω→2f X lt)) x → odef X x
+     eq1 {x} fx = {!!}
+     eq2 : {x : Ordinal} → odef X x → odef (fω→2 (ω→2f X lt)) x
+     eq2 {x} Xx = {!!}
+  
+fω→2-iso : (f : Nat → Two) → ω→2f ( fω→2 f ) (ω2f f) ≡ f
+fω→2-iso f = f-extensionality (λ x → eq1 x ) where
+     eq1 : (x : Nat) → ω→2f (fω→2 f) (ω2f f) x ≡ f x
+     eq1 x = {!!}
+
+
 ↑n : (f n : HOD) → ((ω→2 ∋ f ) ∧ (infinite ∋ n)) → HOD
 ↑n f n lt = 3→Hω2 ( ω→2f f (proj1 lt) 3↑ (ω→nat n (proj2 lt) ))