# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595230092 -32400
# Node ID 6c72bee25653271bb6ca135de2c8870ca8fa7fd5
# Parent  8cade5f660bd1f2b32162de254483fc2dbab418f
...

diff -r 8cade5f660bd -r 6c72bee25653 BAlgbra.agda
--- a/BAlgbra.agda	Mon Jul 20 16:22:44 2020 +0900
+++ b/BAlgbra.agda	Mon Jul 20 16:28:12 2020 +0900
@@ -1,4 +1,3 @@
-{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Ordinals
 module BAlgbra {n : Level } (O : Ordinals {n})   where
@@ -56,13 +55,13 @@
     lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B
        (record { proj1 = case2 refl ; proj2 = subst (λ k → odef B k) (sym diso) B∋x}))
 
-∩-Select : { A B : HOD } →  Select A (  λ x _ → ( A ∋ x ) ∧ ( B ∋ x )  ) ≡ ( A ∩ B )
+∩-Select : { A B : HOD } →  Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  ) ≡ ( A ∩ B )
 ∩-Select {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } ) where
-    lemma1 : {x : Ordinal} → odef (Select A (λ x₁ _ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x
-    lemma1 {x} lt = record { proj1 = proj1 {!!} ; proj2 = subst (λ k → odef B k ) diso (proj2 (proj2 {!!} )) }
-    lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ _ → (A ∋ x₁) ∧ (B ∋ x₁))) x
-    lemma2 {x} lt = {!!} -- record { proj1 = proj1 lt ; proj2 =
-        -- record { proj1 = subst (λ k → odef A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → odef B k ) (sym diso) (proj2 lt) } }
+    lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x
+    lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → odef B k ) diso (proj2 (proj2 lt)) }
+    lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x
+    lemma2 {x} lt = record { proj1 = proj1 lt ; proj2 =
+        record { proj1 = subst (λ k → odef A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → odef B k ) (sym diso) (proj2 lt) } }
 
 dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡   ( p ∩ q ) ∪ ( p ∩ r )
 dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
diff -r 8cade5f660bd -r 6c72bee25653 LEMC.agda
--- a/LEMC.agda	Mon Jul 20 16:22:44 2020 +0900
+++ b/LEMC.agda	Mon Jul 20 16:28:12 2020 +0900
@@ -40,12 +40,12 @@
     ; _∋_ = _∋_ 
     ; _≈_ = _=h=_ 
     ; ∅  = od∅
-    ; Select = {!!}
+    ; Select = Select
     ; isZFC = isZFC
  } where
     -- infixr  200 _∈_
     -- infixr  230 _∩_ _∪_
-    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ {!!}
+    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ Select
     isZFC = record {
        choice-func = λ A {X} not A∋X → a-choice (choice-func X not );
        choice = λ A {X} A∋X not → is-in (choice-func X not)
diff -r 8cade5f660bd -r 6c72bee25653 OD.agda
--- a/OD.agda	Mon Jul 20 16:22:44 2020 +0900
+++ b/OD.agda	Mon Jul 20 16:28:12 2020 +0900
@@ -156,9 +156,6 @@
 _c<_ : ( x a : HOD  ) → Set n
 x c< a = a ∋ x 
 
-d→∋ : ( a : HOD  ) { x : Ordinal} → odef a x → a ∋ (ord→od x)
-d→∋ a lt = subst (λ k → odef a k ) (sym diso) lt
-
 cseq :  HOD  →  HOD 
 cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
     lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x)
@@ -260,11 +257,11 @@
 odmax<od→ord  : { x y : HOD } → x ∋ y →  Set n
 odmax<od→ord {x} {y} x∋y = odmax x o< od→ord x
 
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
--- postulate f-extensionality : { n m : Level}  → Relation.Binary.PropositionalEquality.Extensionality n m
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+-- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
 
-in-codomain : (X : HOD  ) → ( ψ : (x : HOD ) → X ∋ x → HOD  ) → OD 
-in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( (y<X : odef X y ) →   ( x ≡ od→ord (ψ (ord→od y ) (d→∋ X y<X)))))  }
+in-codomain : (X : HOD  ) → ( ψ : HOD  → HOD  ) → OD 
+in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ( x ≡ od→ord (ψ (ord→od y )))))  }
 
 _∩_ : ( A B : HOD ) → HOD 
 A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x }
@@ -329,15 +326,13 @@
      ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
      ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy
 
-Select : (X : HOD  ) → ((x : HOD  ) → X ∋ x → Set n ) → HOD 
-Select X ψ = record { od = record { def = λ x →  odef X x ∧ ( (x<X : odef X x ) →  ψ ( ord→od x ) (d→∋ X x<X) ) } ; odmax = odmax X ;
-    <odmax = λ y → <odmax X (proj1 y) }
-
-Replace : (X : HOD  ) → ((x : HOD) → X ∋ x → HOD) → HOD 
-Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y) (d→∋ X X∋y )))) ∧ def (in-codomain X ψ) x }
+Select : (X : HOD  ) → ((x : HOD  ) → Set n ) → HOD 
+Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
+Replace : HOD  → (HOD  → HOD) → HOD 
+Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) ∧ def (in-codomain X ψ) x }
     ; odmax = rmax ; <odmax = rmax<} where 
         rmax : Ordinal
-        rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y) (d→∋ X X∋y ) ))
+        rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))
         rmax< :  {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax
         rmax< lt = proj1 lt
 Union : HOD  → HOD   
@@ -363,7 +358,7 @@
 OPwr  A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( A ∩ (ord→od x)) ) )   
 
 Power : HOD  → HOD 
-Power A = Replace (OPwr (Ord (od→ord A))) ( λ x _ → A ∩ x )
+Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x )
 -- ｛_｝ : ZFSet → ZFSet
 -- ｛ x ｝ = ( x ,  x )     -- better to use (x , x) directly
 
@@ -462,33 +457,28 @@
     lemma : {y : Ordinal} → odef X y ∧ odef (ord→od y) (od→ord z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z))
     lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → odef X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } 
 
-ψiso : {X : HOD}  {ψ : (x : HOD ) → X ∋ x → Set n} {x y : HOD } → {lt : X ∋ x}{lt' : X ∋ y} → ψ x lt → x ≡ y → lt ≅ lt' → ψ y lt'
-ψiso {X} {ψ} t refl HE.refl = t
-
-selection : {X y : HOD} → {ψ : (x : HOD ) → X ∋ x → Set n} → ((X ∋ y) ∧ ((y∈X : X ∋ y) → ψ y y∈X)) ⇔ (Select X ψ ∋ y)
-selection  {X} {y} {ψ} = record {
-    proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = λ x<X → ψiso {X} {ψ} (proj2 cond (proj1 cond)) (sym oiso) {!!}  }
-  ; proj2 = λ select → {!!} -- record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
-  } where
-      lemma : {X x : HOD} ( x<X : X ∋ x) → x<X ≅ d→∋ X x<X
-      lemma {X} {x} x<X with (oiso {x} )
-      ... | t = {!!}
-
-sup-c< :  {X x : HOD} → (ψ : (y : HOD ) → X ∋ y → HOD) → (X∋x : X ∋ x ) → od→ord (ψ x X∋x ) o< (sup-o X (λ y X∋y → od→ord (ψ (ord→od y) {!!} )))
-sup-c< {X} {x} ψ lt = subst (λ k → od→ord (ψ k {!!} ) o< _ ) oiso (sup-o< X lt )
-replacement← : (X x : HOD) →  {ψ : (y : HOD )→ X ∋ y  → HOD} → (X∋x : X ∋ x ) → Replace X ψ ∋ ψ x {!!}
-replacement←  X x {ψ} lt = record { proj1 =  sup-c<  {X} {x} ψ lt ; 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 oiso)} ))
-replacement→ : (X x : HOD) {ψ : (y : HOD ) → X ∋ y → HOD}  → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y {!!} ))
-replacement→  X x {ψ} lt = contra-position lemma (lemma2 {!!} ) where
-    lemma2 :  ¬ ((y : Ordinal) → ¬ odef X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y) {!!} )))
-            → ¬ ((y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y) {!!} ))
+ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
+ψiso {ψ} t refl = t
+selection : {ψ : HOD → Set n} {X y : HOD} → ((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  }
+  }
+sup-c< :  (ψ : HOD → HOD) → {X x : HOD} → X ∋ x  → od→ord (ψ x) o< (sup-o X (λ y X∋y → od→ord (ψ (ord→od y))))
+sup-c< ψ {X} {x} lt = subst (λ k → od→ord (ψ k) o< _ ) oiso (sup-o< X lt )
+replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
+replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {X} {x} lt ; 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 oiso)} ))
+replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
+replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
+    lemma2 :  ¬ ((y : Ordinal) → ¬ odef X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y))))
+            → ¬ ((y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od 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→od  y) {!!} )) → (ord→od (od→ord x) =h= ψ (ord→od y) {!!})  
+        lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od  y))) → (ord→od (od→ord x) =h= ψ (ord→od y))  
         lemma3 {y} eq = subst (λ k  → ord→od (od→ord x) =h= k ) oiso (o≡→== eq )
-    lemma :  ( (y : HOD) → ¬ (x =h= ψ y {!!} )) → ( (y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y) {!!} ) )
-    lemma not y not2 = not (ord→od y) (subst (λ k → k =h= ψ (ord→od y) {!!} ) oiso  ( proj2 not2 ))
+    lemma :  ( (y : HOD) → ¬ (x =h= ψ y)) → ( (y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y)) )
+    lemma not y not2 = not (ord→od y) (subst (λ k → k =h= ψ (ord→od y)) oiso  ( proj2 not2 ))
 
 ---
 --- Power Set
@@ -537,7 +527,7 @@
 power→ A t P∋t {x} t∋x = FExists _ lemma5 lemma4 where
     a = od→ord A
     lemma2 : ¬ ( (y : HOD) → ¬ (t =h=  (A ∩ y)))
-    lemma2 = replacement→  (OPwr (Ord (od→ord A))) t {λ x _ → A ∩ x} P∋t
+    lemma2 = replacement→ {λ x → A ∩ x} (OPwr (Ord (od→ord A))) t P∋t
     lemma3 : (y : HOD) → t =h= ( A ∩ y ) → ¬ ¬ (A ∋ x)
     lemma3 y eq not = not (proj1 (eq→ eq t∋x))
     lemma4 : ¬ ((y : Ordinal) → ¬ (t =h= (A ∩ ord→od y)))
@@ -611,8 +601,8 @@
     lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))
     lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A)))  (λ x lt → od→ord (A ∩ (ord→od x))))
         lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 )
-    lemma2 :  def (in-codomain (OPwr (Ord (od→ord A))) {!!} ) (od→ord t)
-    lemma2 not = ⊥-elim ( not (od→ord t) {!!}  ) where
+    lemma2 :  def (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t)
+    lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
         lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) 
         lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym oiso) ( ∩-≡ {t} {A} t→A  )))
 
@@ -665,9 +655,9 @@
     ;   ε-induction = ε-induction 
     ;   infinity∅ = infinity∅
     ;   infinity = infinity
-    ;   selection = λ {X}  {y} {ψ} → selection {X} {y} {ψ}
-    ;   replacement← = {!!} -- replacement←
-    ;   replacement→ = {!!} -- λ {ψ} → replacement→ {ψ}
+    ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
+    ;   replacement← = replacement←
+    ;   replacement→ = λ {ψ} → replacement→ {ψ}
     -- ;   choice-func = choice-func
     -- ;   choice = choice
     } 
diff -r 8cade5f660bd -r 6c72bee25653 ODC.agda
--- a/ODC.agda	Mon Jul 20 16:22:44 2020 +0900
+++ b/ODC.agda	Mon Jul 20 16:28:12 2020 +0900
@@ -93,12 +93,12 @@
     ; _∋_ = _∋_ 
     ; _≈_ = _=h=_ 
     ; ∅  = od∅
-    ; Select = {!!}
+    ; Select = Select
     ; isZFC = isZFC
  } where
     -- infixr  200 _∈_
     -- infixr  230 _∩_ _∪_
-    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ {!!}
+    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ Select
     isZFC = record {
        choice-func = choice-func ;
        choice = choice
diff -r 8cade5f660bd -r 6c72bee25653 OPair.agda
--- a/OPair.agda	Mon Jul 20 16:22:44 2020 +0900
+++ b/OPair.agda	Mon Jul 20 16:28:12 2020 +0900
@@ -156,7 +156,7 @@
     lemma | tri> ¬a ¬b c = {!!}
 
 _⊗_ : (A B : HOD) → HOD
-A ⊗ B  = Union ( Replace B (λ b _ → Replace A (λ a _ → < a , b > ) ))
+A ⊗ B  = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
 
 product→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ( A ⊗ B ) ∋ < a , b >
 product→ {A} {B} {a} {b} A∋a B∋b = {!!}
diff -r 8cade5f660bd -r 6c72bee25653 cardinal.agda
--- a/cardinal.agda	Mon Jul 20 16:22:44 2020 +0900
+++ b/cardinal.agda	Mon Jul 20 16:28:12 2020 +0900
@@ -34,10 +34,10 @@
 ∋-p A x | case1 t = yes t
 ∋-p A x | case2 t = no t
 
-_⊗_  : (A B : HOD) → HOD
-A ⊗ B  = record { od = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } } where
-    checkAB : { p : Ordinal } → def ZFProduct p → Set n
-    checkAB (pair x y) = odef A x ∧ odef B y
+--_⊗_  : (A B : HOD) → HOD
+--A ⊗ B  = record { od = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } } where
+--    checkAB : { p : Ordinal } → def ZFProduct p → Set n
+--    checkAB (pair x y) = odef A x ∧ odef B y
 
 func→od0  : (f : Ordinal → Ordinal ) → HOD
 func→od0  f = record { od = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkfunc p ) }}  where
@@ -64,7 +64,7 @@
    lemma : Ordinal → Ordinal → Ordinal
    lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → odef (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y)
    lemma x y | p | no n  = o∅
-   lemma x y | p | yes f∋y = lemma2 (proj1 (ODC.double-neg-eilm O ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) 
+   lemma x y | p | yes f∋y = lemma2 ? where -- (ODC.double-neg-eilm O ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) 
            lemma2 : {p : Ordinal} → ord-pair p  → Ordinal
            lemma2 (pair x1 y1) with ODC.decp O ( x1 ≡ x)
            lemma2 (pair x1 y1) | yes p = y1
diff -r 8cade5f660bd -r 6c72bee25653 zf.agda
--- a/zf.agda	Mon Jul 20 16:22:44 2020 +0900
+++ b/zf.agda	Mon Jul 20 16:28:12 2020 +0900
@@ -16,8 +16,8 @@
      (_,_ : ( A B : ZFSet  ) → ZFSet)
      (Union : ( A : ZFSet  ) → ZFSet)
      (Power : ( A : ZFSet  ) → ZFSet)
-     (Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → (X ∋ x) → Set m ) → ZFSet ) 
-     (Replace : (X : ZFSet) → ( (x : ZFSet ) → ( X ∋ x ) → ZFSet ) → ZFSet )
+     (Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet ) 
+     (Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet )
      (infinite : ZFSet)
        : Set (suc (n ⊔ suc m)) where
   field
@@ -33,7 +33,7 @@
   _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set m
   _⊆_ A B {x} = A ∋ x →  B ∋ x
   _∩_ : ( A B : ZFSet  ) → ZFSet
-  A ∩ B = Select A (  λ x _ → ( A ∋ x ) ∧ ( B ∋ x )  )
+  A ∩ B = Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
   _∪_ : ( A B : ZFSet  ) → ZFSet
   A ∪ B = Union (A , B)    
   ｛_｝ : ZFSet → ZFSet
@@ -55,10 +55,10 @@
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
      infinity∅ :  ∅ ∈ infinite
      infinity :  ∀( x : ZFSet  ) → x ∈ infinite →  ( x ∪ ｛ x ｝) ∈ infinite 
-     selection : ∀ { X y : ZFSet  } →  { ψ : (x : ZFSet ) → X ∋ x → Set m } → (y ∈ X ∧ (( y∈X : y ∈ X ) →  ψ y y∈X)) ⇔ (y ∈ Select X ψ ) 
+     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← : ∀ ( X x : ZFSet  ) → (x∈X : x ∈ X ) → {ψ : (x : ZFSet ) → x ∈ X  → ZFSet} → ψ x x∈X ∈  Replace X ψ 
-     replacement→ : ∀ ( X x : ZFSet  ) →  {ψ : (x : ZFSet ) → X ∋ x  → ZFSet} → ( lt : x ∈  Replace X ψ ) → ¬ ( ∀ (y : ZFSet)  → (X∋y : X ∋ y ) →  ¬ ( x ≈ ψ y 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 ) )
 
 record ZF {n m : Level } : Set (suc (n ⊔ suc m)) where
   infixr  210 _,_
@@ -73,8 +73,8 @@
      _,_ : ( A B : ZFSet  ) → ZFSet
      Union : ( A : ZFSet  ) → ZFSet
      Power : ( A : ZFSet  ) → ZFSet
-     Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → ( X ∋ x ) → Set m ) → ZFSet 
-     Replace : (X : ZFSet ) → ( (x : ZFSet ) → ( X ∋ x ) → ZFSet ) → ZFSet
+     Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet 
+     Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet
      infinite : ZFSet
      isZF : IsZF ZFSet _∋_ _≈_ ∅ _,_ Union Power Select Replace infinite