# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1562559674 -32400
# Node ID 3ba37037faf44a9ee13c43a0a660d033b0cc2dba
# Parent  21b9e78e93598600931067f76175852d53172b01
Union again

diff -r 21b9e78e9359 -r 3ba37037faf4 HOD.agda
--- a/HOD.agda	Mon Jul 08 12:34:08 2019 +0900
+++ b/HOD.agda	Mon Jul 08 13:21:14 2019 +0900
@@ -292,22 +292,22 @@
     ; infinite = Ord omega
     ; isZF = isZF 
  } where
+    ZFSet = OD {suc n}
     Select : (X : OD {suc n} ) → ((x : OD {suc n} ) → Set (suc n) ) → OD {suc n}
     Select X ψ = record { def = λ x →  ( def X  x ∧  ψ ( ord→od x )) }
     Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n}
     Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
     _,_ : OD {suc n} → OD {suc n} → OD {suc n}
     x , y = Ord (omax (od→ord x) (od→ord y))
+    _∩_ : ( A B : ZFSet  ) → ZFSet
+    A ∩ B = record { def = λ x → def A x ∧ def B x } -- Select (A , B) (  λ x → ( A ∋ x ) ∧ (B ∋ x) )
     Union : OD {suc n} → OD {suc n}
-    Union U = cseq U 
+    Union U = Replace ( record { def = λ x → osuc x o< od→ord U } )  ( λ x → U ∩ x ) 
     -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x →  X ∋ x )
-    ZFSet = OD {suc n}
     _∈_ : ( A B : ZFSet  ) → Set (suc n)
     A ∈ B = B ∋ A
     _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set (suc n)
     _⊆_ A B {x} = A ∋ x →  B ∋ x
-    _∩_ : ( A B : ZFSet  ) → ZFSet
-    A ∩ B = record { def = λ x → def A x ∧ def B x } -- Select (A , B) (  λ x → ( A ∋ x ) ∧ (B ∋ x) )
     Power : OD {suc n} → OD {suc n}
     Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
     -- _∪_ : ( A B : ZFSet  ) → ZFSet
@@ -346,6 +346,48 @@
          empty x (case1 ())
          empty x (case2 ())
 
+         union-lemma : {n : Level } {X z u : OD {suc n} } → (X ∋ u) → (u ∋ z) → osuc ( od→ord z ) o< od→ord u → X ∋ Ord (osuc ( od→ord z ) )
+         union-lemma = {!!}
+         union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
+         union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) )
+         union→ :  (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
+         union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z ))
+         union→ X z u xx | tri< a ¬b ¬c with  osuc-< a (c<→o< (proj2 xx))
+         union→ X z u xx | tri< a ¬b ¬c | ()
+         union→ X z u xx | tri≈ ¬a b ¬c = {!!}
+         union→ X z u xx | tri> ¬a ¬b c = {!!}  --- osuc ( od→ord z )) o<  od→ord u o< od→ord X
+            -- def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (union-lemma {n} {X} {z} {u} (proj1 xx) (proj2 xx) c ) refl (sym ord-Ord)
+         union← :  (X z : OD) (X∋z : Union X ∋ z) → (X ∋  union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z )
+         union← X z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where
+             lemma : X ∋ union-u {X} {z} X∋z
+             lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} {!!} refl ord-Ord
+
+         ψiso :  {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y   → ψ y
+         ψiso {ψ} t refl = t
+         selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
+         selection {ψ} {X} {y} = record {
+              proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso)  }
+            ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
+           }
+         replacement← : {ψ : OD → OD} (X x : OD) →  X ∋ x → Replace X ψ ∋ ψ x
+         replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {x} ; proj2 = lemma } where
+             lemma : def (in-codomain X ψ) (od→ord (ψ x))
+             lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k))
+                 (sym (subst (λ k → Ord (od→ord x) ≡ k) oiso (Ord-ord) )) } ))
+         replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
+         replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
+            lemma2 :  ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (Ord y))))
+                    → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)))
+            lemma2 not not2  = not ( λ y d →  not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
+                lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (Ord y))) → (ord→od (od→ord x) == ψ (Ord y))  
+                lemma3 {y} eq = subst (λ k  → ord→od (od→ord x) == k ) oiso (o≡→== eq )
+            lemma :  ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)) )
+            lemma not y not2 = not (Ord y) (subst (λ k → k == ψ (Ord y)) oiso  ( proj2 not2 ))
+
+         ---
+         --- Power Set
+         ---
+         ---    First consider ordinals in OD
          ---
          --- ZFSubset A x =  record { def = λ y → def A y ∧  def x y }                   subset of A
          --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )       Power X is a sup of all subset of A
@@ -409,42 +451,9 @@
               lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x)))
               lemma = sup-o<   
 
-         union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
-         union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) )
-         union→ :  (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
-         union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z ))
-         union→ X z u xx | tri< a ¬b ¬c with  osuc-< a (c<→o< (proj2 xx))
-         union→ X z u xx | tri< a ¬b ¬c | ()
-         union→ X z u xx | tri≈ ¬a b ¬c = def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (proj1 xx) refl b 
-         union→ X z u xx | tri> ¬a ¬b c = {!!}     --- osuc ( od→ord z )) o<  od→ord u o< od→ord X
-
-         union← :  (X z : OD) (X∋z : Union X ∋ z) → (X ∋  union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z )
-         union← X z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where
-             lemma : X ∋ union-u {X} {z} X∋z
-             lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} X∋z refl ord-Ord
-
-         ψiso :  {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y   → ψ y
-         ψiso {ψ} t refl = t
-         selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
-         selection {ψ} {X} {y} = record {
-              proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso)  }
-            ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
-           }
-         replacement← : {ψ : OD → OD} (X x : OD) →  X ∋ x → Replace X ψ ∋ ψ x
-         replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {x} ; proj2 = lemma } where
-             lemma : def (in-codomain X ψ) (od→ord (ψ x))
-             lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k))
-                 (sym (subst (λ k → Ord (od→ord x) ≡ k) oiso (Ord-ord) )) } ))
-         replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
-         replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
-            lemma2 :  ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (Ord y))))
-                    → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)))
-            lemma2 not not2  = not ( λ y d →  not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
-                lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (Ord y))) → (ord→od (od→ord x) == ψ (Ord y))  
-                lemma3 {y} eq = subst (λ k  → ord→od (od→ord x) == k ) oiso (o≡→== eq )
-            lemma :  ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)) )
-            lemma not y not2 = not (Ord y) (subst (λ k → k == ψ (Ord y)) oiso  ( proj2 not2 ))
-
+         -- 
+         -- Every set in OD is a subset of Ordinals
+         -- 
          -- Power A = Replace (Def (Ord (od→ord A))) ( λ y → A ∩ y )
          power→ :  ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
          power→ A t P∋t {x} t∋x = TransFiniteExists {suc n} {λ y → (t ==  (A ∩ ord→od y))}
@@ -499,7 +508,7 @@
               lemma : {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ≡ osuc y o< osuc (osuc (od→ord x)) 
               lemma {y} = let open ≡-Reasoning in begin
                    def (Union (x , (x , x))) y  
-                ≡⟨⟩
+                ≡⟨ {!!} ⟩
                    def ( Ord ( omax (od→ord x) (od→ord (Ord (omax (od→ord x)  (od→ord x)  )) ))) ( osuc y )
                 ≡⟨⟩
                    osuc y o<  omax (od→ord x) (od→ord (Ord (omax (od→ord x)  (od→ord x)  )) )
diff -r 21b9e78e9359 -r 3ba37037faf4 ordinal.agda
--- a/ordinal.agda	Mon Jul 08 12:34:08 2019 +0900
+++ b/ordinal.agda	Mon Jul 08 13:21:14 2019 +0900
@@ -314,11 +314,14 @@
       caseOSuc lx ox (TransFinite caseΦ caseOSuc  record { lv = lx ; ord = ox })
 
 --  (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p )  → p
-TransFiniteExists : {n : Level} → { ψ : Ordinal {n} → Set n } 
+--      may be we can prove this...
+postulate 
+ TransFiniteExists : {n : Level} → { ψ : Ordinal {n} → Set n } 
   → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
   → {p : Set n} ( P : { y : Ordinal {n} } →  ψ y → p )
   → p
-TransFiniteExists {n} {ψ} exists {p} P = ⊥-elim ( exists lemma ) where
-    lemma : (y : Ordinal {n} ) → ¬ ψ y
-    lemma y ψy = ( TransFinite {n} {{!!}} {!!} {!!} y ) ψy
+
+-- TransFiniteExists {n} {ψ} exists {p} P = ⊥-elim ( exists lemma ) where
+--     lemma : (y : Ordinal {n} ) → ¬ ψ y
+--     lemma y ψy = ( TransFinite {n} {{!!}} {!!} {!!} y ) ψy