--- a/ordinal-definable.agda	Sun Jun 02 10:53:52 2019 +0900
+++ b/ordinal-definable.agda	Sun Jun 02 11:56:43 2019 +0900
@@ -242,6 +242,9 @@
 ∅< {n} {x} {y} d eq | lift ()
        
 
+def-iso : {n : Level} {A B : OD {n}} {x y : Ordinal {n}} → x ≡ y  → (def A y → def B y)  → def A x → def B x
+def-iso refl t = t
+
 is-od∅ : {n : Level} →  ( x : OD {suc n} ) → Dec ( x == od∅ {suc n} )
 is-od∅ {n} x with trio< {n} (od→ord x) (o∅ {suc n})
 is-od∅ {n} x | tri≈ ¬a b ¬c = yes ( ∅7 (orefl b) ) 
@@ -335,9 +338,9 @@
        ;   union→ = union→
        ;   union← = union←
        ;   empty = empty
-       ;   power→ = {!!}
-       ;   power← = {!!}
-       ;   extensionality = {!!}
+       ;   power→ = power→
+       ;   power← = power← 
+       ;   extensionality = extensionality
        ;   minimul = minimul
        ;   regularity = regularity
        ;   infinity∅ = {!!}
@@ -352,6 +355,17 @@
          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→ : (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)
+             lemma1 = {!!}
+             lemma2 : def (ord→od y) (od→ord t)
+             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 ) )
          union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → union-u X z U>z  ∋ z
@@ -386,3 +400,6 @@
             reg : {y : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) y → def od∅ y
             reg {y} t with proj1 t
             ... | x∈∅ = x∈∅
+         extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
+         eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
+         eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d