--- 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  ≈ ∅ ) )