# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559444203 -32400
# Node ID 8e8f54e7a030659eba8db172895182915ad48ae0
# Parent  714470702a8b88d9c377e6510a766009713733f9
extensionality done

diff -r 714470702a8b -r 8e8f54e7a030 ordinal-definable.agda
--- 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  
diff -r 714470702a8b -r 8e8f54e7a030 zf.agda
--- a/zf.agda	Sun Jun 02 10:53:52 2019 +0900
+++ b/zf.agda	Sun Jun 02 11:56:43 2019 +0900
@@ -70,7 +70,7 @@
      power→ : ∀( A t : ZFSet  ) → Power A ∋ t → ∀ {x}  →  _⊆_ t A {x} 
      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 z  : ZFSet  } → (( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B
+     extensionality :  { A B : ZFSet  } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z)  ) → A ≈ B
      -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
      minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet 
      regularity : ∀( x : ZFSet  ) → (not : ¬ (x ≈ ∅)) → (  minimul x not  ∈ x ∧  (  minimul x not  ∩ x  ≈ ∅ ) )