--- a/OD.agda	Mon Jul 20 16:28:12 2020 +0900
+++ b/OD.agda	Mon Jul 20 17:08:16 2020 +0900
@@ -328,6 +328,7 @@
 
 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 
@@ -335,6 +336,21 @@
         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
+
+d→∋ : ( a : HOD  ) { x : Ordinal} → odef a x → a ∋ (ord→od x)
+d→∋ a lt = subst (λ k → odef a k ) (sym diso) lt
+
+in-codomain' : (X : HOD  ) → ((x : HOD) → X ∋ x → HOD) → OD 
+in-codomain'  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ((lt : odef X y) →  x ≡ od→ord (ψ (ord→od y ) (d→∋ X lt) ))))  }
+
+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 }
+      ; odmax = rmax ; <odmax = rmax< } where
+        rmax : Ordinal
+        rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y) (d→∋ X X∋y)))
+        rmax< :  {y : Ordinal} → (y o< rmax) ∧ def (in-codomain' X ψ) y → y o< rmax
+        rmax< lt = proj1 lt
+
 Union : HOD  → HOD   
 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x)))  }
     ; odmax = osuc (od→ord U) ; <odmax = umax< } where
@@ -464,6 +480,7 @@
     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
@@ -480,6 +497,22 @@
     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 ))
 
+sup-c<' :  {X x : HOD} → (ψ : (x : 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←' : (X x : HOD) {ψ : (x : 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 = ? }))
+replacement→' :  (X x : HOD) → {ψ : (x : HOD) → X ∋ x → HOD} → (lt : Replace' X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y ? ))
+replacement→'  X x {ψ} lt = contra-position lemma (lemma2 (λ lt1 → ? )) 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} 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 ))
+
 ---
 --- Power Set
 ---