--- a/zf.agda	Mon Jun 10 09:50:52 2019 +0900
+++ b/zf.agda	Wed Jun 12 10:45:00 2019 +0900
@@ -21,6 +21,9 @@
 open import Relation.Nullary
 open import Relation.Binary
 
+contra-position : {n : Level } {A B : Set n} → (A → B) → ¬ B → ¬ A 
+contra-position {n} {A} {B}  f ¬b a = ¬b ( f a ) 
+
 infixr  130 _∧_
 infixr  140 _∨_
 infixr  150 _⇔_
@@ -52,7 +55,7 @@
   _∩_ : ( A B : ZFSet  ) → ZFSet
   A ∩ B = Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
   _∪_ : ( A B : ZFSet  ) → ZFSet
-  A ∪ B = Union (A , B) 
+  A ∪ B = Union (A , B)    -- Select A (  λ x → ( A ∋ x ) ∨ ( B ∋ x )  ) is easer
   ｛_｝ : ZFSet → ZFSet
   ｛ x ｝ = ( x ,  x )
   infixr  200 _∈_
@@ -74,6 +77,9 @@
      selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet  } →  ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈  Select X ψ ) 
      -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
      replacement : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( ψ x ∈  Replace X ψ )  
+   -- -- ∀ z [ ∀ x ( x ∈ z  → ¬ ( x ≈ ∅ ) )  ∧ ∀ x ∀ y ( x , y ∈ z ∧ ¬ ( x ≈ y )  → x ∩ y ≈ ∅  ) → ∃ u ∀ x ( x ∈ z → ∃ t ( u ∩ x) ≈ ｛ t ｝) ]
+   -- axiom-of-choice : Set (suc n) 
+   -- axiom-of-choice = ?
 
 record ZF {n m : Level } : Set (suc (n ⊔ m)) where
   infixr  210 _,_