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