# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559309423 -32400
# Node ID 93abc0133b8a50923cb1973b1b5ba0886edc47ef
# Parent  c69657d0055709a39aa5344a6f4684bc975f5aaa
union continue

diff -r c69657d00557 -r 93abc0133b8a ordinal-definable.agda
--- a/ordinal-definable.agda	Thu May 30 02:31:58 2019 +0900
+++ b/ordinal-definable.agda	Fri May 31 22:30:23 2019 +0900
@@ -106,13 +106,13 @@
 def-subst : {n : Level } {Z : OD {n}} {X : Ordinal {n} }{z : OD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
 def-subst df refl refl = df
 
-transitive : {n : Level } { z y x : OD {n} } → z ∋ y → y ∋ x → z  ∋ x
-transitive  {n} {z} {y} {x} z∋y x∋y  with  ordtrans ( c<→o< {n} {x} {y} x∋y ) (  c<→o< {n} {y} {z} z∋y ) 
+transitive : {n : Level } { z y x : OD {suc n} } → z ∋ y → y ∋ x → z  ∋ x
+transitive  {n} {z} {y} {x} z∋y x∋y  with  ordtrans ( c<→o< {suc n} {x} {y} x∋y ) (  c<→o< {suc n} {y} {z} z∋y ) 
 ... | t = lemma0 (lemma t) where
    lemma : ( od→ord x ) o< ( od→ord z ) → def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x )))
    lemma xo<z = o<→c< xo<z
    lemma0 :  def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x ))) →  def z (od→ord x)
-   lemma0 dz  = def-subst {n} { ord→od ( od→ord z )} { od→ord ( ord→od ( od→ord x))} dz (oiso) (diso)
+   lemma0 dz  = def-subst {suc n} { ord→od ( od→ord z )} { od→ord ( ord→od ( od→ord x))} dz (oiso) (diso)
 
 record Minimumo {n : Level } (x : Ordinal {n}) : Set (suc n) where
   field
@@ -279,7 +279,9 @@
          lemma1 = cong ( λ k → od→ord k ) o∅→od∅
      lemma o∅ ne | yes refl | ()
      lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅→od∅ (o<→c< (∅5 ¬p))  
-      
+
+-- ∃-set :  {n : Level} → ( x : OD {suc n} ) → ( ψ :  OD {suc n} → Set (suc n) ) → Set (suc n)
+-- ∃-set = {!!}
 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality (suc (suc n)) (suc (suc n ))
 
@@ -310,7 +312,7 @@
     _,_ : OD {suc n} → OD {suc n} → OD {suc n}
     x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) }
     Union : OD {suc n} → OD {suc n}
-    Union x = record { def = λ y → {z : Ordinal {suc n}} → def x z  → def (ord→od z) y  }
+    Union U = record { def = λ y → y o< (od→ord U) }
     Power : OD {suc n} → OD {suc n}
     Power x = record { def = λ y → (z : Ordinal {suc n} ) → ( def x y ∧ def (ord→od z) y )  }
     ZFSet = OD {suc n}
@@ -329,8 +331,8 @@
     isZF = record {
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
        ;   pair  = pair
-       ;   union→ = {!!}
-       ;   union← = {!!}
+       ;   union-u = {!!}
+       ;   union-iso = {!!}
        ;   empty = empty
        ;   power→ = {!!}
        ;   power← = {!!}
@@ -349,8 +351,18 @@
          proj2 (pair A B ) =  case2 refl 
          empty : (x : OD {suc n} ) → ¬  (od∅ ∋ x)
          empty x ()
-         union→ :  (X x y : OD) → X ∋ x → x ∋ y → Union X ∋ y
-         union→ X x y X∋x x∋y {z} X∋z  = {!!} -- transitive {suc n} {X} {x} {y} X∋x x∋y  
+         union→ :  (X x y : OD {suc n}) → X ∋ x → x ∋ y → Union X ∋ y
+         union→ X x y X∋x x∋y =  c<→o<  (transitive {n} {X} {x} {y} X∋x x∋y  )
+         union-u : (X z : OD {suc n}) → OD {suc n}
+         union-u X z = record { def =  ( λ u → (u o< od→ord X)  ∧ (od→ord z o< u) ) }
+         union-iso :  (X z : OD {suc n}) → (Union X ∋ z) ⇔ ((Union X ∋ union-u X z ) ∧ (union-u X z ∋ z))
+         --    ((x : OD) →  (z ∋ x → y ∋ x)) → y ∋ z 
+         proj1 ( union-iso X z ) U∋z = record { proj1 = U∋u ;  proj2 = u∋z } where
+             U∋u : Union X ∋ union-u X z
+             U∋u = {!!}
+             u∋z : union-u X z ∋ z
+             u∋z = {!!}
+         proj2 (union-iso X z ) U∋u∧U∋z  = transitive {n} {!!} {!!} -- (proj1 U∋u∧U∋z ) (proj2 U∋u∧U∋z )
          ψ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)
diff -r c69657d00557 -r 93abc0133b8a zf.agda
--- a/zf.agda	Thu May 30 02:31:58 2019 +0900
+++ b/zf.agda	Fri May 31 22:30:23 2019 +0900
@@ -49,9 +49,9 @@
      isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_ 
      -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z)
      pair : ( A B : ZFSet  ) →  ( (A , B)  ∋ A ) ∧ ( (A , B)  ∋ B  )
-     -- ∀ X ∃ A∀ t(t ∈ A ⇔ ∃ x ∈ X(t  ∈ x))
-     union→ : ( X x y : ZFSet  ) → X ∋ x  → x ∋ y → Union X  ∋ y
-     union← : ( X x y : ZFSet  ) → Union X  ∋ y → X ∋ x  → x ∋ y 
+     -- ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x  ∧ (z ∈ u))
+     union-u : ( y z : ZFSet  ) → ZFSet
+     union-iso : ( X z : ZFSet ) → (Union X ∋ z ) ⇔ ((Union X ∋ union-u X z )  ∧ (union-u X z ∋ z ))
   _∈_ : ( A B : ZFSet  ) → Set m
   A ∈ B = B ∋ A
   _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set m
@@ -69,7 +69,7 @@
      power→ : ∀( A t : ZFSet  ) → Power A ∋ t → ∀ {x}  →  _⊆_ t A {x} 
      power← : ∀( A t : ZFSet  ) → ∀ {x}  →  _⊆_ t A {x}  → Power A ∋ t 
      -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
-     extensionality :  ( A B z  : ZFSet  ) → (( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B
+     extensionality :  { A B z  : ZFSet  } → (( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B
      -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
      minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet 
      regularity : ∀( x : ZFSet  ) → (not : ¬ (x ≈ ∅)) → (  minimul x not  ∈ x ∧  (  minimul x not  ∩ x  ≈ ∅ ) )