--- a/zf.agda	Sun Jul 07 08:56:25 2019 +0900
+++ b/zf.agda	Sun Jul 07 17:37:26 2019 +0900
@@ -22,8 +22,8 @@
 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 ) 
+contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A 
+contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a ) 
 
 infixr  130 _∧_
 infixr  140 _∨_
@@ -78,7 +78,7 @@
      selection : ∀ { X : ZFSet  } →  { ψ : (x : ZFSet ) →  Set m } → ∀ {  y : ZFSet  } →  (((y : ZFSet) → y ∈ X → ψ y ) ∧ ( y ∈ X ) ) ⇔ (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 ∈ X → ψ x ∈  Replace X ψ 
-     replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( lt : x ∈  Replace X ψ ) → ¬ ( ∀ (y : ZFSet)  →  ¬ ( ψ x ≈ y ) )
+     replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( lt : x ∈  Replace X ψ ) → ¬ ( ∀ (y : ZFSet)  →  ¬ ( x ≈ ψ y ) )
    -- -- ∀ 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 = ?