--- a/OPair.agda	Wed Jul 29 12:42:05 2020 +0900
+++ b/OPair.agda	Wed Jul 29 21:51:00 2020 +0900
@@ -137,37 +137,28 @@
 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< 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 x<y with osuc-≡< (pair-xx<xy {x} {y})
-    lemma1 x<y | case1 eq = ⊥-elim ( o<¬≡ (cong (λ k → od→ord k ) (xx=zy→x=y (ord→== eq))) x<y ) 
-    lemma1 x<y | case2 lt = lt
-    lemma0 : od→ord x o< od→ord y → od→ord < x , y > o< next o∅
-    lemma0 x<y = osucprev (begin
+ω-pair {x} {y} lx ly = lemma0 where
+    lemma3 : od→ord (x , y) o< next o∅
+    lemma3 = next< (omax<nx (<odmax infinite lx) (<odmax infinite ly)) ho<
+    lemma0 : od→ord < x , y > o< next o∅
+    lemma0 = osucprev (begin
          osuc (od→ord < x , y >)
        <⟨ osuc<nx ho< ⟩
          next (omax (od→ord (x , x)) (od→ord (x , y)))
-       ≡⟨ cong (λ k → next k ) (sym (omax< _ _ (lemma1 x<y))) ⟩
+       ≡⟨ cong (λ k → next k) (sym ( omax≤ _ _ pair-xx<xy )) ⟩
          next (osuc (od→ord (x , y)))
        ≡⟨ sym (nexto≡) ⟩
          next (od→ord (x , y))
-       ≤⟨ osucprev (ordtrans (next< ( omax<nx (<odmax infinite lx) (<odmax infinite ly))  (osuc<nx lemma2 )) (ordtrans <-osuc <-osuc )) ⟩
+       ≤⟨ x<ny→≤next lemma3 ⟩
          next o∅
        ∎ ) where
           open o≤-Reasoning O
-          lemma2 : next (od→ord (x , y)) o< next (omax (od→ord x) (od→ord y))
-          lemma2 = {!!}
-    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 > ) ))
 
-product→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ( A ⊗ B ) ∋ < a , b >
-product→ {A} {B} {a} {b} A∋a B∋b = {!!}
+-- product→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ( A ⊗ B ) ∋ < a , b >
+-- product→ {A} {B} {a} {b} A∋a B∋b = λ t → t (od→ord (Select (A ⊗ B) (λ x → x =h= < a , b >))) record { proj1 = {!!} ; proj2 = {!!} }
 
 record IsProduct (A B p : HOD) (A⊗B∋p : (A ⊗ B ) ∋ p )  : Set (suc n) where
   field
@@ -175,10 +166,10 @@
     π1A : A ∋ π1 is-pair 
     π2B : B ∋ π2 is-pair 
 
-product← : {A B a b p : HOD} → (lt : (A ⊗ B ) ∋ p )  → IsProduct A B p lt
-product← lt = record { is-pair = {!!} ; π1A = {!!} ; π2B = {!!} }
+-- product← : {A B a b p : HOD} → (lt : (A ⊗ B ) ∋ p )  → IsProduct A B p lt
+-- product← {_} {_} {a} {b} lt = record { is-pair = {!!} ; π1A = {!!} ; π2B = {!!} }
 
  
-ZFP  : (A B : HOD) → HOD
-ZFP  A B = record { od = record { def = λ x → ord-pair x ∧ ((p : ord-pair x ) → odef A (pi1 p) ∧ odef B (pi2 p) )} ;
-        odmax = omax (odmax A) (odmax B) ; <odmax = λ {y} px → {!!}  } -- (<odmax A (proj2 px (proj1 px) ))
+-- ZFP  : (A B : HOD) → HOD
+-- ZFP  A B = record { od = record { def = λ x → ord-pair x ∧ ((p : ord-pair x ) → odef A (pi1 p) ∧ odef B (pi2 p) )} ;
+--         odmax = omax (odmax A) (odmax B) ; <odmax = λ {y} px → {!!}  } -- (<odmax A (proj2 px (proj1 px) ))