--- a/generic-filter.agda	Sun Jul 26 21:10:37 2020 +0900
+++ b/generic-filter.agda	Sun Jul 26 21:39:27 2020 +0900
@@ -86,18 +86,11 @@
 HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where
     P  : (i j : Nat) (x : Ordinal ) → HOD
     P  i j x = ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) , ord→od x
-    nat0 : (i : Nat) → od→ord (nat→ω i) o< next o∅ 
-    nat0 i = <odmax infinite (ω∋nat→ω {i})
-    lemma3 : (i j : Nat) → od→ord ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) o< next o∅ 
-    lemma3 i j = pair-<xy (pair-<xy (nat0 i) (nat0 i) ) (pair-<xy (nat0 i) (nat0 j) )
+    nat1 : (i : Nat) (x : Ordinal) → od→ord (nat→ω i) o< next x
+    nat1 i x =  next< nexto∅ ( <odmax infinite (ω∋nat→ω {i}))
     lemma1 : (i j : Nat) (x : Ordinal ) → osuc (od→ord (P i j x)) o< next x
-    lemma1 i j x = osuc<nx ( next< lemma2 ho<  ) where
-       lemma2 :  odmax (((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) , ord→od x) o< next x
-       lemma2 with trio<  (od→ord ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j))) (od→ord (ord→od x))
-           |   inspect (omax (od→ord ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)))) (od→ord (ord→od x))
-       lemma2 | tri< a ¬b ¬c | _ = osuc<nx (subst (λ k → k o< next x ) (sym diso) x<nx )
-       lemma2 | tri≈ ¬a b ¬c | record { eq = eq1 } = subst₂ (λ j k → j o< next k ) (trans (omax≡  _ _ b ) eq1 ) diso (osuc<nx x<nx)
-       lemma2 | tri> ¬a ¬b c | record { eq = eq1 } =  osuc<nx ( next< nexto∅ (lemma3 i j))
+    lemma1 i j x = osuc<nx (pair-<xy (pair-<xy (pair-<xy (nat1 i x) (nat1 i x) ) (pair-<xy (nat1 i x) (nat1 j x) ) )
+         (subst (λ k → k o< next x) (sym diso) x<nx ))
     lemma : (i j : Nat) (x : Ordinal ) → od→ord (Union (P i j x)) o< next x
     lemma i j x = next< (lemma1 i j x ) ho<
     odmax0 :  {y : Ordinal} → Hω2r y → y o< next o∅ 
@@ -124,19 +117,16 @@
    lemma record { count = (Suc i) ; hω2 = (he hω3) } = nothing ∷ lemma record { count = i ; hω2 =  hω3 }
 
 ω→2 : HOD
-ω→2 = Replace (Power infinite) (λ p  → Replace infinite (λ 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
+ω→2 = Power infinite
 
 ω→2f : (x : HOD) → ω→2 ∋ x → Nat → Two
-ω→2f x = {!!}
+ω→2f x lt n with ODC.∋-p O x (nat→ω n)
+ω→2f x lt n | yes p = i1
+ω→2f x lt n | no ¬p = i0
 
 ↑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) ))
 
-
 record CountableOrdinal : Set (suc (suc n)) where
    field
        ctl→ : Nat → Ordinal