--- a/OD.agda	Thu Aug 29 16:08:46 2019 +0900
+++ b/OD.agda	Thu Aug 29 16:16:51 2019 +0900
@@ -171,6 +171,70 @@
 is-o∅ x | tri≈ ¬a b ¬c = yes b
 is-o∅ x | tri> ¬a ¬b c = no ¬b
 
+_,_ : OD  → OD  → OD 
+x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } --  Ord (omax (od→ord x) (od→ord y))
+<_,_> : (x y : OD) → OD
+< x , y > = (x , x ) , (x , y )
+
+exg-pair : { x y : OD } → (x , y ) == ( y , x )
+exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
+    left : {z : Ordinal} → def (x , y) z → def (y , x) z 
+    left (case1 t) = case2 t
+    left (case2 t) = case1 t
+    right : {z : Ordinal} → def (y , x) z → def (x , y) z 
+    right (case1 t) = case2 t
+    right (case2 t) = case1 t
+
+==-trans : { x y z : OD } →  x == y →  y == z →  x ==  z
+==-trans x=y y=z  = record { eq→ = λ {m} t → eq→ y=z (eq→ x=y t) ; eq← =  λ {m} t → eq← x=y (eq← y=z t) }
+
+==-sym : { x y  : OD } →  x == y →  y == x 
+==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← =  λ {m} t → eq→ x=y t }
+
+ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y
+ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq )
+
+od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y
+od≡→≡ eq = subst₂ (λ j k → j ≡ k ) diso diso ( cong ( λ k → od→ord k ) eq )
+
+eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
+eq-prod refl refl = refl
+
+prod-eq : { x x' y y' : OD } → < x , y > == < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
+prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where
+    lemma0 : {x y z : OD } → ( x , x ) == ( z , y ) → x ≡ y
+    lemma0 {x} {y} eq with trio< (od→ord x) (od→ord y) 
+    lemma0 {x} {y} eq | tri< a ¬b ¬c with eq← eq {od→ord y} (case2 refl) 
+    lemma0 {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a )
+    lemma0 {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a )
+    lemma0 {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b
+    lemma0 {x} {y} eq | tri> ¬a ¬b c  with eq← eq {od→ord y} (case2 refl) 
+    lemma0 {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c )
+    lemma0 {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c )
+    lemma2 : {x y z : OD } → ( x , x ) == ( z , y ) → z ≡ y
+    lemma2 {x} {y} {z} eq = trans (sym (lemma0 lemma3 )) ( lemma0 eq )  where
+        lemma3 : ( x , x ) == ( y , z )
+        lemma3 = ==-trans eq exg-pair
+    lemma1 : {x y : OD } → ( x , x ) == ( y , y ) → x ≡ y
+    lemma1 {x} {y} eq with eq← eq {od→ord y} (case2 refl)
+    lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s)
+    lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s)
+    lemma4 : {x y z : OD } → ( x , y ) == ( x , z ) → y ≡ z
+    lemma4 {x} {y} {z} eq with eq← eq {od→ord z} (case2 refl)
+    lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z
+    ... | refl with lemma2 (==-sym eq )
+    ... | refl = refl
+    lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z
+    lemmax : x ≡ x'
+    lemmax with eq→ eq {od→ord (x , x)} (case1 refl) 
+    lemmax | case1 s = lemma1 (ord→== s )  -- (x,x)≡(x',x')
+    lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y'
+    ... | refl = lemma1 (ord→== s )
+    lemmay : y ≡ y'
+    lemmay with lemmax
+    ... | refl with lemma4 eq -- with (x,y)≡(x,y')
+    ... | eq1 = lemma4 (ord→== (cong (λ  k → od→ord k )  eq1 ))
+
 ppp :  { p : Set n } { a : OD  } → record { def = λ x → p } ∋ a → p
 ppp  {p} {a} d = d
 
@@ -268,8 +332,6 @@
     Select X ψ = record { def = λ x →  ( def X x ∧ ψ ( ord→od x )) }
     Replace : OD  → (OD  → OD  ) → OD 
     Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
-    _,_ : OD  → OD  → OD 
-    x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } --  Ord (omax (od→ord x) (od→ord y))
     _∩_ : ( A B : ZFSet  ) → ZFSet
     A ∩ B = record { def = λ x → def A x ∧ def B x } 
     Union : OD  → OD   
@@ -533,7 +595,6 @@
                         }
          
 
-_,_ = ZF._,_ OD→ZF
 Union = ZF.Union OD→ZF
 Power = ZF.Power OD→ZF
 Select = ZF.Select OD→ZF