--- a/OPair.agda	Sun Jul 19 00:26:55 2020 +0900
+++ b/OPair.agda	Sun Jul 19 03:24:39 2020 +0900
@@ -135,24 +135,25 @@
 p-pi2 :  { x y : HOD } → (p : def ZFProduct (od→ord  < x , y >) ) →  π2 p ≡ y
 p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p)))
 
-ω-pair : {x y : HOD} → infinite ∋ x → infinite ∋ y → od→ord < x , y > o< osuc (next o∅)
-ω-pair {x} {y} lx ly with trio< (od→ord x) (od→ord y)
-ω-pair {x} {y} lx ly | tri≈ ¬a b ¬c = {!!}
-ω-pair {x} {y} lx ly | tri< a ¬b ¬c = {!!}
-ω-pair {x} {y} lx ly | tri> ¬a ¬b c = {!!}
--- ω-pair {x} {y} lx ly = begin
---       od→ord < x , y >
---     <⟨ ho< ⟩
---       next (omax (od→ord (x , x)) (od→ord (x , y)))
---     ≤⟨ {!!} ⟩
---       next (omax (od→ord (x , x)) (od→ord (x , y)))
---     ≡⟨ cong (λ k → next k ) (sym (omax< _ _ {!!} )) ⟩
---       next (osuc (od→ord (x , y)))
---     ≤⟨ {!!} ⟩
---       od→ord < ord→od (next o∅)  , ord→od (next o∅)  >
---     ≤⟨ {!!} ⟩
---       next o∅ 
---     ∎ where open o≤-Reasoning O
+ω-pair : {x y : HOD} → infinite ∋ x → infinite ∋ y → od→ord < x , y > o< next o∅
+ω-pair {x} {y} lx ly = lemma where
+    lemma1 : od→ord x o< od→ord y → od→ord ( x , x ) o< od→ord ( x , y ) 
+    lemma1 = {!!}
+    lemma0 : od→ord x o< od→ord y → od→ord < x , y > o< osuc (next (od→ord (x , y)))
+    lemma0 x<y = begin
+         od→ord < x , y >
+       <⟨ ho< ⟩
+         next (omax (od→ord (x , x)) (od→ord (x , y)))
+       ≡⟨ cong (λ k → next k ) (sym (omax< _ _ (lemma1 x<y))) ⟩
+         next (osuc (od→ord (x , y)))
+       ≡⟨ sym (nexto≡) ⟩
+         next (od→ord (x , y))
+       ∎ where open o≤-Reasoning O
+    lemma : od→ord < x , y > o< next o∅
+    lemma  with trio< (od→ord x) (od→ord y)
+    lemma | tri< a ¬b ¬c = {!!}
+    lemma | tri≈ ¬a b ¬c = next< {!!} {!!}
+    lemma | tri> ¬a ¬b c = {!!}
 
 _⊗_ : (A B : HOD) → HOD
 A ⊗ B  = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))

--- a/filter.agda	Sun Jul 19 00:26:55 2020 +0900
+++ b/filter.agda	Sun Jul 19 03:24:39 2020 +0900
@@ -124,10 +124,10 @@
 record Dense  (P : HOD ) : Set (suc n) where
    field
        dense : HOD
-       incl :  dense ⊆ P 
+       incl :  dense ⊆ Power P 
        dense-f : HOD → HOD
-       dense-d :  { p : HOD} → P ∋ p  → dense ∋ dense-f p  
-       dense-p :  { p : HOD} → P ∋ p  →  p ⊆ (dense-f p) 
+       dense-d :  { p : HOD} → p ⊆ P → dense ∋ dense-f p  
+       dense-p :  { p : HOD} → p ⊆ P → p ⊆ (dense-f p) 
 
 record Ideal  ( L : HOD  ) : Set (suc n) where
    field
@@ -184,8 +184,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
 
-HODω2-Filter : Filter HODω2
-HODω2-Filter = record {
+data Two : Set n where
+   i0 : Two
+   i1 : Two
+
+record ω2r : Set n where
+   field
+     func2 : Nat → Two
+     ω2 : {!!}
+
+ω→2 : HOD
+ω→2 = Replace infinite (λ x → < x , {!!} > )
+
+G : (Nat → Two) → Filter HODω2
+G f = record {
        filter = {!!}
      ; f⊆PL = {!!}
      ; filter1 = {!!}
@@ -202,10 +214,6 @@
 
 -- the set of finite partial functions from ω to 2
 
-data Two : Set n where
-   i0 : Two
-   i1 : Two
-
 Hω2f : Set (suc n)
 Hω2f = (Nat → Set n) → Two