--- a/ordinal-definable.agda	Sun Jun 02 11:56:43 2019 +0900
+++ b/ordinal-definable.agda	Sun Jun 02 15:12:26 2019 +0900
@@ -283,15 +283,6 @@
      lemma o∅ ne | yes refl | ()
      lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅→od∅ (o<→c< (∅5 ¬p))  
 
--- ∃-set :  {n : Level} → ( x : OD {suc n} ) → ( ψ :  OD {suc n} → Set (suc n) ) → Set (suc n)
--- ∃-set = {!!}
-
--- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality (suc (suc n)) (suc (suc n ))
-
--- ==∅→≡ :  {n : Level} →  { x : OD {suc n} } → (  x  == od∅ {suc n} ) → x ≡ od∅ {suc n} 
--- ==∅→≡ {n} {x} eq = cong (  λ k → record { def = k } ) (trans {!!} ∅-base-def ) where
-
-
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
@@ -316,8 +307,9 @@
     x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) }
     Union : OD {suc n} → OD {suc n}
     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 → (z : Ordinal {suc n} ) → ( def x y ∧ def (ord→od z) y )  }
+    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
@@ -355,16 +347,14 @@
          proj2 (pair A B ) =  case2 refl 
          empty : (x : OD {suc n} ) → ¬  (od∅ ∋ x)
          empty x ()
-         --    Power x = record { def = λ y → (z : Ordinal {suc n} ) → ( def x y ∧ def (ord→od z) y )  }
+         --- 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 = transitive {n} {A} {t} {x} lemma t∋x  where
-             lemma : A ∋ t
-             lemma = proj1 (P∋t (od→ord x )) 
-         power← : (A t : OD) {x : OD} → (t ∋ x → A ∋ x) → Power A ∋ t
-         power← A t {x} t→A y = record { proj1 = lemma1 ; proj2 = lemma2 } where
-             lemma1 : def A (od→ord t)
+         power→ A t P∋t {x} t∋x = proj1 (P∋t (od→ord 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 (ord→od y) (od→ord t)
+             lemma2 : def A z
              lemma2 = {!!}
          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 ) )