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

--- a/zf.agda	Sun Jun 02 11:56:43 2019 +0900
+++ b/zf.agda	Sun Jun 02 15:12:26 2019 +0900
@@ -11,23 +11,15 @@
       proj1 : A
       proj2 : B
 
-open _∧_
-
-
 data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
    case1 : A → A ∨ B
    case2 : B → A ∨ B
 
--- open import Relation.Binary.PropositionalEquality 
-
 _⇔_ : {n : Level } → ( A B : Set n )  → Set  n
-_⇔_ A B =  ( A → B ) ∧ ( B  → A )
+_⇔_ A B =  ( A → B ) ∧ ( B → A )
 
-open import Data.Empty
 open import Relation.Nullary
-
 open import Relation.Binary
-open import Relation.Binary.Core
 
 infixr  130 _∧_
 infixr  140 _∨_
@@ -68,7 +60,7 @@
      empty :  ∀( x : ZFSet  ) → ¬ ( ∅ ∋ x )
      -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
      power→ : ∀( A t : ZFSet  ) → Power A ∋ t → ∀ {x}  →  _⊆_ t A {x} 
-     power← : ∀( A t : ZFSet  ) → ∀ {x}  →  _⊆_ t A {x}  → Power A ∋ t 
+     power← : ∀( A t : ZFSet  ) → ( ∀ {x}  →  _⊆_ t A {x})  → Power A ∋ t 
      -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
      extensionality :  { A B : ZFSet  } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z)  ) → A ≈ B
      -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
@@ -99,20 +91,3 @@
      infinite : ZFSet
      isZF : IsZF ZFSet _∋_ _≈_ ∅ _,_ Union Power Select Replace infinite 
 
-module zf-exapmle {n m : Level } ( zf : ZF {m} {n} ) where
-
-  _≈_ =  ZF._≈_ zf
-  ZFSet =  ZF.ZFSet  zf
-  Select =  ZF.Select  zf
-  ∅ =  ZF.∅ zf
-  _∩_ =  ( IsZF._∩_  ) (ZF.isZF zf)
-  _∋_ =   ZF._∋_  zf
-  replacement =   IsZF.replacement  ( ZF.isZF zf )
-  selection =   IsZF.selection  ( ZF.isZF zf )
-  minimul =   IsZF.minimul  ( ZF.isZF zf )
-  regularity =   IsZF.regularity  ( ZF.isZF zf )
-
---  russel : Select ( λ x →  x ∋ x  ) ≈ ∅
---  russel with Select ( λ x →  x ∋ x  ) 
---  ... | s = {!!}
-