--- a/ordinal-definable.agda	Tue Jun 04 12:28:43 2019 +0900
+++ b/ordinal-definable.agda	Tue Jun 04 23:58:58 2019 +0900
@@ -254,7 +254,7 @@
     Select : OD {suc n} → (OD {suc n} → Set (suc n) ) → OD {suc n}
     Select X ψ = record { def = λ x →  ( def X  x ∧  ψ ( ord→od x )) } 
     _,_ : OD {suc n} → OD {suc n} → OD {suc n}
-    x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) }
+    x , y = record { def = λ z → z o< (omax (od→ord x) (od→ord y)) }
     Union : OD {suc n} → OD {suc n}
     Union U = record { def = λ y → osuc y o< (od→ord U) }
     -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x →  X ∋ x )
@@ -293,8 +293,8 @@
          open _∧_ 
          open Minimumo
          pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧  ((A , B) ∋ B)
-         proj1 (pair A B ) =  case1 refl 
-         proj2 (pair A B ) =  case2 refl 
+         proj1 (pair A B ) = omax-x {n} {od→ord A} {od→ord B}
+         proj2 (pair A B ) = omax-y {n} {od→ord A} {od→ord B}
          empty : (x : OD {suc n} ) → ¬  (od∅ ∋ x)
          empty x ()
          --- Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → ( def X x ∧ def (ord→od y) x )  }
@@ -343,29 +343,20 @@
          extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
          eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
          eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d  
-         pair-or : {x y : OD {suc n} } → (x , x) ∋ y → (y == x ) ∨ (x ∋ y )
-         pair-or {x} {y} lt with tri-c< x y
-         pair-or {x} {y} lt | tri< a ¬b ¬c = {!!}   --     x < y < ( x ,  x )
-         pair-or {x} {y} lt | tri≈ ¬a b ¬c = case1 (eq-sym b)
-         pair-or {x} {y} lt | tri> ¬a ¬b c = case2 c
-         pair-osuc : (x : OD) →  od→ord (x , x) ≡ osuc (od→ord x)
-         pair-osuc x with trio< (od→ord (x , x)) (osuc (od→ord x))
-         pair-osuc x | tri< a ¬b ¬c = ⊥-elim ( osuc-<  a (c<→o< (proj1 (pair x x )) ))
-         pair-osuc x | tri≈ ¬a b ¬c = b
-         pair-osuc x | tri> ¬a ¬b c with pair-or (def-subst (o<→c<  c ) oiso refl ) --  (x , x)  ∋ ord→od (osuc (od→ord x) )
-         pair-osuc x | tri> ¬a ¬b c | case1 eq = ⊥-elim ( o<→¬== (def-subst {suc n} (o<→c<  c ) refl diso ) eq )
-         pair-osuc x | tri> ¬a ¬b c | case2 lt = ⊥-elim (c<> c lt ) where
-             lemma2 : (z : Ordinal {suc n} ) → lv (od→ord (ord→od z , ord→od z) ) ≡ lv z
-             lemma2 z = {!!}
+         pair-osuc : {x y : OD {suc n}} →  (x , x)  ∋ y →  (od→ord y ) o< osuc (od→ord x) 
+         pair-osuc {x} {y} z with union← (x , x) y z
+         ... | t = {!!}
          next : (x : OD) → Union (x , (x , x)) == ord→od (osuc (od→ord x))
-         eq→ (next x ) {y} z = {!!}
+         eq→ (next x ) {y} z = {!!}       --   z : y o< osuc (osuc ox ) → y < osuc ox
          eq← (next x ) {y} z = def-subst {suc n} {_} {_} {Union (x , (x , x))} {_}
                   (union→ (x , (x , x)) (ord→od y) (ord→od (osuc y)) (record { proj1 = lemma1 ; proj2 = lemma2 } )) refl diso where
+             lemma0 :  (x , x) ∋ ord→od y 
+             lemma0 = o<-subst {suc n} {od→ord (ord→od y)} {od→ord {!!}} (c<→o< z) {!!} {!!}
              lemma1 : (x , (x , x)) ∋ ord→od (osuc y)    -- z : def (ord→od (osuc (od→ord x))) y
-             lemma1 with tri-c< (x , x) (ord→od (osuc (od→ord x)))
-             lemma1 | tri< a ¬b ¬c = {!!}
-             lemma1 | tri≈ ¬a b ¬c = {!!}
-             lemma1 | tri> ¬a ¬b c = {!!}
+             lemma1 with osuc-≡< {suc n} (def-subst {suc n} (o<→c< z) oiso refl)
+             lemma1 | case1 x = {!!}
+             lemma1 | case2 t = {!!}
+             -- = o<-subst (c<→o< {suc n} {_} {ord→od y} {!!} ) {!!} {!!}
              lemma2 : ord→od (osuc y) ∋ ord→od y
              lemma2 = o<→c< <-osuc
          next' : (x : OD) →  ord→od ( od→ord ( Union (x , (x , x)))) == ord→od (osuc (od→ord x))