--- a/HOD.agda	Tue Jul 02 09:28:26 2019 +0900
+++ b/HOD.agda	Tue Jul 02 15:59:07 2019 +0900
@@ -342,7 +342,10 @@
        ;   infinity∅ = infinity∅
        ;   infinity = λ _ → infinity
        ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
-       ;   replacement = replacement
+       ;   reverse = ?
+       ;   reverse-∈ = ?
+       ;   replacement← = ?
+       ;   replacement→ = ?
      } where
 
          pair : (A B : HOD {suc n} ) → ((A , B) ∋ A) ∧  ((A , B) ∋ B)
@@ -375,6 +378,7 @@
               minsup =  ZFSubset (Ord a) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))) 
               Ltx :   {n : Level} → {x t : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
               Ltx {n} {x} {t} lt = c<→o< lt
+              -- lemma1 hold because minsup is Ord (minα a sp) 
               lemma1 : od→ord (Ord (od→ord t)) o< od→ord minsup → minsup ∋ Ord (od→ord t)
               lemma1 lt with OrdSubset a ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))
               ... | eq with subst ( λ k →  ZFSubset (Ord a) k ≡ Ord (minα a sp)) Ord-ord eq
@@ -391,7 +395,6 @@
                     ≡⟨ sym eq1 ⟩
                       minsup
                     ∎
-
          -- 
          -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t
          -- Power A is a sup of ZFSubset A t, so Power A ∋ t
@@ -410,10 +413,18 @@
               lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x)))
               lemma = sup-o<   
 
+         -- Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
          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← = {!!}
+         power← A t t→A = def-subst {suc n} {Replace (Def (Ord a)) ψ} {_} {Power A} {od→ord t} (sup-c< ψ {t}) lemma2 lemma1 where
+              a = od→ord A
+              ψ : HOD → HOD
+              ψ y = Def (Ord a) ∩ y
+              lemma1 : od→ord (Def (Ord a) ∩ t) ≡ od→ord t
+              lemma1 = {!!} 
+              lemma2 : Ord ( sup-o ( λ x → od→ord (ψ (ord→od x )))) ≡ Power A
+              lemma2 = {!!}
 
          union-u : {X z : HOD {suc n}} → (U>z : Union X ∋ z ) → HOD {suc n}
          union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) )