changeset 247:d09437fcfc7c

fix pair
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 26 Aug 2019 12:27:20 +0900
parents 3506f53c7d83
children 9fd85b954477
files OD.agda cardinal.agda zf.agda
diffstat 3 files changed, 55 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Mon Aug 26 02:50:16 2019 +0900
+++ b/OD.agda	Mon Aug 26 12:27:20 2019 +0900
@@ -269,7 +269,7 @@
     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 = Ord (omax (od→ord x) (od→ord y))
+    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   
@@ -294,7 +294,8 @@
     isZF : IsZF (OD )  _∋_  _==_ od∅ _,_ Union Power Select Replace infinite
     isZF = record {
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
-       ;   pair  = pair
+       ;   pair→  = pair→
+       ;   pair←  = pair←
        ;   union→ = union→
        ;   union← = union←
        ;   empty = empty
@@ -311,9 +312,17 @@
        ;   choice = choice
      } where
 
-         pair : (A B : OD  ) → ((A , B) ∋ A) ∧  ((A , B) ∋ B)
-         proj1 (pair A B ) = omax-x  (od→ord A) (od→ord B)
-         proj2 (pair A B ) = omax-y  (od→ord A) (od→ord B)
+         pair→ : ( x y t : ZFSet  ) →  (x , y)  ∋ t  → ( t == x ) ∨ ( t == y ) 
+         pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡x ))
+         pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡y ))
+
+         pair← : ( x y t : ZFSet  ) → ( t == x ) ∨ ( t == y ) →  (x , y)  ∋ t  
+         pair← x y t (case1 t==x) = case1 (cong (λ k → od→ord k ) (==→o≡ t==x))
+         pair← x y t (case2 t==y) = case2 (cong (λ k → od→ord k ) (==→o≡ t==y))
+
+         -- pair0 : (A B : OD  ) → ((A , B) ∋ A) ∧  ((A , B) ∋ B)
+         -- proj1 (pair A B ) = omax-x  (od→ord A) (od→ord B)
+         -- proj2 (pair A B ) = omax-y  (od→ord A) (od→ord B)
 
          empty : (x : OD  ) → ¬  (od∅ ∋ x)
          empty x = ¬x<0 
--- a/cardinal.agda	Mon Aug 26 02:50:16 2019 +0900
+++ b/cardinal.agda	Mon Aug 26 12:27:20 2019 +0900
@@ -61,13 +61,49 @@
 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 = {!!} where
+--     lemma : < x , y > ≡ < x , y' > → y ≡ y'
+--     lemma eq1 with trio< (od→ord x) (od→ord y) 
+--     lemma eq1 | tri< a ¬b ¬c = {!!}
+--     lemma eq1 | tri≈ ¬a b ¬c = {!!}
+--     lemma eq1 | tri> ¬a ¬b c = {!!}
+
 postulate
    def-eq :  { P Q p q : OD } →  P ≡ Q → p ≡ q → (pt : P ∋ p ) → (qt : Q ∋ q ) → pt ≅ qt
 
+∈-to-ord : {p : Ordinal } → ( ZFProduct ∋  ord→od p ) → ord-pair p
+∈-to-ord {p} lt = def-subst {ZFProduct} {(od→ord (ord→od p))} {_} {_} lt refl diso
+
+ord-to-∈ : {p : Ordinal } → ord-pair p → ZFProduct ∋  ord→od p 
+ord-to-∈ {p} lt = def-subst {_} {_} {ZFProduct} {(od→ord (ord→od p))} lt refl (sym diso)
+
+lemma333 : { A a  : OD } → { x : A ∋ a } → def-subst {A} {od→ord a} (def-subst {A} {od→ord a} x refl refl ) refl refl ≡ x
+lemma333 = refl
+
+lemma334 : { A B  : OD } → {a b : Ordinal} → { x : A ∋ ord→od a } → { y : B ∋ ord→od b } → (f1 : A ≡ B) → (f2 : a ≡ b)
+   → def-subst {B} {od→ord (ord→od b)} (def-subst {A} { od→ord (ord→od a)} x f1 (cong (λ k → od→ord (ord→od k)) f2 )) refl refl ≅ x
+lemma334 {A} {A} {a} {a} {x} {y} refl refl with def-eq {A} {A} {ord→od a} {ord→od a} refl refl x y
+... | HE.refl = HE.refl
+
+lemma335 : { A B C : OD } → {a b c : Ordinal} → { x : A ∋ ord→od a } → { y : C ∋ ord→od c } → (f1 : A ≡ B) → (f2 : a ≡ b) → (g1 : B ≡ C) → (g2 : b ≡ c)
+   → def-subst {B} {od→ord (ord→od b)} (def-subst {A} { od→ord (ord→od a)} x f1 (cong (λ k → od→ord (ord→od k)) f2 )) g1 (cong (λ k → od→ord (ord→od k)) g2 )
+      ≅ def-subst {A} { od→ord (ord→od a)} {C } { od→ord (ord→od c)} x (trans f1 g1)
+          (trans (cong (λ k → od→ord (ord→od k)) f2 ) (cong (λ k → od→ord (ord→od k)) g2 ))
+lemma335 {A} {A} {A} {a} {a} {a} {x} {y} refl refl refl refl with def-eq {A} {A} {ord→od a} {ord→od a} refl refl x y
+... | HE.refl = HE.refl
+
+∈-to-ord-oiso : { p : Ordinal } → { x : ord-pair p } → ∈-to-ord (ord-to-∈ x) ≡ x
+∈-to-ord-oiso {p} {x} = {!!} where
+   lemma : def-subst {_} {_} {ZFProduct} {{!!}} (def-subst {_} {_} {ZFProduct} {{!!}} x refl (sym diso)) refl diso ≡ x
+   lemma = {!!}
+
 lemma34 : { p q : Ordinal } → (x :  ord-pair p ) → (y :  ord-pair q ) → p ≡ q → x ≅ y
-lemma34 {p} {q} x y eq = {!!} where
+lemma34 {p} {q} x y refl = subst₂ (λ j k → j ≅ k) ∈-to-ord-oiso ∈-to-ord-oiso (HE.cong (λ k → ∈-to-ord k) lemma1 ) where
    lemma : (pt : ZFProduct ∋ ord→od p ) → (qt : ZFProduct ∋ ord→od q ) → p ≡ q → pt ≅ qt
-   lemma pt qt eq = def-eq {ZFProduct} {ZFProduct} refl {!!} {!!} {!!}
+   lemma pt qt eq = def-eq {ZFProduct} {ZFProduct} refl (cong (λ k → ord→od k) eq) pt qt
+   lemma1 : (ord-to-∈ x) ≅ (ord-to-∈ y )
+   lemma1 = lemma (ord-to-∈ x) (ord-to-∈ y ) refl
 
 π1-cong :  { p q : OD } →  p ≡ q → (pt : ZFProduct ∋ p ) → (qt : ZFProduct ∋ q ) → π1 pt ≅ π1 qt
 π1-cong {p} {q} refl s t = HE.cong (λ k → pi1 k ) (def-eq {ZFProduct} {ZFProduct} refl refl s t ) 
--- a/zf.agda	Mon Aug 26 02:50:16 2019 +0900
+++ b/zf.agda	Mon Aug 26 12:27:20 2019 +0900
@@ -22,8 +22,9 @@
        : Set (suc (n ⊔ m)) where
   field
      isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_ 
-     -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z)
-     pair : ( A B : ZFSet  ) →  ( (A , B)  ∋ A ) ∧ ( (A , B)  ∋ B  )
+     -- ∀ x ∀ y ∃ z ∀ t ( z ∋ t → t ≈ x ∨ t  ≈ y)
+     pair→ : ( x y t : ZFSet  ) →  (x , y)  ∋ t  → ( t ≈ x ) ∨ ( t ≈ y ) 
+     pair← : ( x y t : ZFSet  ) →  ( t ≈ x ) ∨ ( t ≈ y )  →  (x , y)  ∋ t 
      -- ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x  ∧ (z ∈ u))
      union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
      union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) →  ¬  ( (u : ZFSet ) → ¬ ((X ∋  u) ∧ (u ∋ z )))