--- a/ordinal-definable.agda	Wed Jun 05 18:24:40 2019 +0900
+++ b/ordinal-definable.agda	Thu Jun 06 09:36:41 2019 +0900
@@ -284,7 +284,7 @@
     Union U = record { def = λ y → osuc y o< (od→ord U) }
     -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x →  X ∋ x )
     Power : OD {suc n} → OD {suc n}
-    Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → ( def X x ∧ def (ord→od y) x )  }
+    Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → def X x → def (ord→od y) x  }
     ZFSet = OD {suc n}
     _∈_ : ( A B : ZFSet  ) → Set (suc n)
     A ∈ B = B ∋ A
@@ -311,9 +311,9 @@
        ;   minimul = minimul
        ;   regularity = regularity
        ;   infinity∅ = infinity∅
-       ;   infinity = {!!}
+       ;   infinity = λ _ → infinity
        ;   selection = λ {ψ} {X} {y} → selection {ψ} {X} {y}
-       ;   replacement = {!!}
+       ;   replacement = replacement
      } where
          open _∧_ 
          open Minimumo
@@ -322,15 +322,11 @@
          proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B)
          empty : (x : OD {suc n} ) → ¬  (od∅ ∋ x)
          empty x ()
-         --- Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → ( def X x ∧ def (ord→od y) x )  }
+         --- Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) →  def X x → def (ord→od y) x  }
          power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
-         power→ A t P∋t {x} t∋x = proj1 (P∋t (od→ord x) ) 
+         power→ A t P∋t {x} t∋x = {!!}
          power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
-         power← A t t→A z = record { proj1 = lemma2 ; proj2 = lemma1 } where
-             lemma1 : def (ord→od (od→ord t)) z
-             lemma1 = {!!}
-             lemma2 : def A z
-             lemma2 = {!!}
+         power← A t t→A z = {!!}
          union-u : (X z : OD {suc n}) → Union X ∋ z → OD {suc n}
          union-u X z U>z = ord→od ( osuc ( od→ord z ) )
          union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → union-u X z U>z  ∋ z
@@ -354,6 +350,8 @@
               proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso)  }
             ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
            }
+         replacement : {ψ : OD → OD} (X x : OD) → Replace X ψ ∋ ψ x
+         replacement {ψ} X x = sup-c< ψ {x}
          ∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
          ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq  
          minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 
@@ -410,6 +408,4 @@
               lemma record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } (case1 (s≤s ()))
               lemma record { lv = 1 ; ord = (Φ 1) } (case2 c2) with d<→lv c2
               lemma record { lv = (Suc Zero) ; ord = (Φ .1) } (case2 ()) | refl
-         replacement : {ψ : OD → OD} (X x : OD) → Replace X ψ ∋ ψ x
-         replacement {ψ} X x = {!!}