# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1562427075 -32400
# Node ID b52683497a2772f3befb0b8f30226b62d7eae03b
# Parent  35ce91192cf499057cb4421126b2baa08853e245
replacement in HOD

diff -r 35ce91192cf4 -r b52683497a27 HOD.agda
--- a/HOD.agda	Sun Jul 07 00:19:01 2019 +0900
+++ b/HOD.agda	Sun Jul 07 00:31:15 2019 +0900
@@ -233,6 +233,9 @@
 csuc :  {n : Level} →  HOD {suc n} → HOD {suc n}
 csuc x = Ord ( osuc ( od→ord x ))
 
+in-codomain : {n : Level} → (X : HOD {suc n} ) → ( ψ : HOD {suc n} → HOD {suc n} ) → HOD {suc n}
+in-codomain {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → ¬ ( def X y ∧  ( x ≡ od→ord (ψ (Ord y )))))  }
+
 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
 
 ZFSubset : {n : Level} → (A x : HOD {suc n} ) → HOD {suc n}
@@ -296,7 +299,7 @@
     ; isZF = isZF 
  } where
     Replace : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n}
-    Replace X ψ = sup-od ψ
+    Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
     Select : (X : HOD {suc n} ) → ((x : HOD {suc n} ) → Set (suc n) ) → HOD {suc n}
     Select X ψ = record { def = λ x → ((y : Ordinal {suc n} ) → X ∋ ord→od y  → ψ (ord→od y)) ∧ (X ∋ ord→od x )  ; otrans = lemma } where
        lemma :  {x : Ordinal} → ((y : Ordinal) → X ∋ ord→od y → ψ (ord→od y)) ∧ (X ∋ ord→od x) →
@@ -342,10 +345,8 @@
        ;   infinity∅ = infinity∅
        ;   infinity = λ _ → infinity
        ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
-       ;   reverse = ?
-       ;   reverse-∈ = ?
-       ;   replacement← = ?
-       ;   replacement→ = ?
+       ;   replacement← = {!!}
+       ;   replacement→ = {!!}
      } where
 
          pair : (A B : HOD {suc n} ) → ((A , B) ∋ A) ∧  ((A , B) ∋ B)
@@ -417,7 +418,7 @@
          power→ :  ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x
          power→ = {!!}
          power← :  (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
-         power← A t t→A = def-subst {suc n} {Replace (Def (Ord a)) ψ} {_} {Power A} {od→ord t} (sup-c< ψ {t}) lemma2 lemma1 where
+         power← A t t→A = def-subst {suc n} {Replace (Def (Ord a)) ψ} {_} {Power A} {od→ord t} {!!} {!!} lemma1 where
               a = od→ord A
               ψ : HOD → HOD
               ψ y = Def (Ord a) ∩ y
@@ -446,9 +447,12 @@
              proj1 = λ y1 y1<X → proj1 s (ord→od y1) y1<X ; proj2 = subst (λ k → def X k ) (sym diso) (proj2 s) }
            ; proj2 = λ s → record { proj1 = λ y1 dy1 → subst (λ k → ψ k ) oiso ((proj1 s) (od→ord y1) (def-subst {suc n} {_} {_} {X} {_} dy1 refl (sym diso )))
                                   ; proj2 = def-subst {suc n} {_} {_} {X} {od→ord y} (proj2 s ) refl diso } } where
-
-         replacement : {ψ : HOD → HOD} (X x : HOD) → Replace X ψ ∋ ψ x
-         replacement {ψ} X x = sup-c< ψ {x}
+         replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
+         replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {x} ; 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 (trans Ord-ord oiso ))} ))
+         replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (ψ x == y))
+         replacement→ {ψ} X x lt not = ⊥-elim ( not (ψ x) (ord→== refl ) )
 
          ∅-iso :  {x : HOD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
          ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq