--- 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
     }