diff cardinal.agda @ 254:2ea2a19f9cd6

ordered pair clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 29 Aug 2019 16:16:51 +0900
parents 0446b6c5e7bc
children 53b7acd63481
line wrap: on
line diff
--- 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 )