# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1567063011 -32400
# Node ID 2ea2a19f9cd638b29af51a47fa3dabdaea381d5c
# Parent  0446b6c5e7bcbd1e7392316f0b80537ef47eecf9
ordered pair clean up

diff -r 0446b6c5e7bc -r 2ea2a19f9cd6 OD.agda
--- 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
diff -r 0446b6c5e7bc -r 2ea2a19f9cd6 cardinal.agda
--- a/cardinal.agda	Thu Aug 29 16:08:46 2019 +0900
+++ b/cardinal.agda	Thu Aug 29 16:16:51 2019 +0900
@@ -20,77 +20,11 @@
 open _∧_
 open _∨_
 open Bool
+open _==_
 
 -- we have to work on Ordinal to keep OD Level n
 -- since we use p∨¬p which works only on Level n
-
-<_,_> : (x y : OD) → OD
-< x , y > = (x , x ) , (x , y )
-
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
-
-
-open _==_
-
-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 ))
-
+--   < x , y > = (x , x) , (x , y)
 
 data ord-pair : (p : Ordinal) → Set n where
    pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )
@@ -98,8 +32,9 @@
 ZFProduct : OD
 ZFProduct = record { def = λ x → ord-pair x }
 
-eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y'
-eq-pair refl refl = HE.refl
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+-- eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y'
+-- eq-pair refl refl = HE.refl
 
 pi1 : { p : Ordinal } →   ord-pair p →  Ordinal
 pi1 ( pair x y) = x
@@ -126,11 +61,9 @@
 p-iso1 {ox} {oy} = pair ox oy
 
 p-iso :  { x  : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
-p-iso {x} p = ord≡→≡ (lemma2 p) where
+p-iso {x} p = ord≡→≡ (lemma p) where
     lemma :  { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op
     lemma (pair ox oy) = refl
-    lemma2 : { x  : OD } → (p : ZFProduct ∋ x ) → od→ord < ord→od (π1 p) , ord→od (π2 p) > ≡ od→ord x
-    lemma2 {x} p = lemma p
 
     
 ∋-p : (A x : OD ) → Dec ( A ∋ x )