# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559145767 -32400
# Node ID 164ad5a703d8fb0435f62e3d8203100e93b64591
# Parent  87df00599a0e19f26e2c0bbdefa9038af45c57c8
¬∅=→∅∈ :  {n : Level} →  { x : OD {suc n} } → ¬ (  x  == od∅ {suc n} ) → x ∋ od∅ {suc n}
¬∅=→∅∈  {n} {x} ne = def-subst (lemma (od→ord x) (subst (λ k → ¬ (k == od∅ {suc n} )) (sym oiso) ne )) oiso refl where
     lemma : (ox : Ordinal {suc n}) →  ¬ (ord→od  ox  == od∅ {suc n} ) → ord→od ox ∋ od∅ {suc n}
     lemma ox = TransFinite {suc n} {λ ox → ¬ (ord→od  ox  == od∅ {suc n} ) → ord→od ox ∋ od∅ {suc n} } { }0 { }1 { }2 ox

diff -r 87df00599a0e -r 164ad5a703d8 ordinal-definable.agda
--- a/ordinal-definable.agda	Wed May 29 18:50:57 2019 +0900
+++ b/ordinal-definable.agda	Thu May 30 01:02:47 2019 +0900
@@ -221,6 +221,16 @@
 tri-c< {n} x y | tri≈ ¬a b ¬c = tri≈ (o≡→¬c< b) (ord→== b) (o≡→¬c< (sym b))
 tri-c< {n} x y | tri> ¬a ¬b c = tri>  ( o<→¬c> c) (λ eq → o<→¬== c (eq-sym eq ) ) (def-subst (o<→c< c) oiso diso)
 
+¬∅=→∅∈ :  {n : Level} →  { x : OD {suc n} } → ¬ (  x  == od∅ {suc n} ) → x ∋ od∅ {suc n} 
+¬∅=→∅∈  {n} {x} ne = def-subst (lemma (od→ord x) (subst (λ k → ¬ (k == od∅ {suc n} )) (sym oiso) ne )) oiso refl where
+     lemma : (ox : Ordinal {suc n}) →  ¬ (ord→od  ox  == od∅ {suc n} ) → ord→od ox ∋ od∅ {suc n}
+     lemma ox = TransFinite {suc n} {λ ox → ¬ (ord→od  ox  == od∅ {suc n} ) → ord→od ox ∋ od∅ {suc n} } {!!} {!!} {!!} ox
+
+-- 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
+
 c<> : {n : Level } { x y : OD {suc n}} → x c<  y  → y c< x  →  ⊥
 c<> {n} {x} {y} x<y y<x with tri-c< x y
 c<> {n} {x} {y} x<y y<x | tri< a ¬b ¬c = ¬c y<x
@@ -317,7 +327,7 @@
        ;   empty = empty
        ;   power→ = {!!}
        ;   power← = {!!}
-       ;   extentionality = {!!}
+       ;   extensionality = {!!}
        ;   minimul = minimul
        ;   regularity = regularity
        ;   infinity∅ = {!!}
@@ -345,7 +355,7 @@
            }
          ∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
          ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq  
-         minord : (x : OD {suc n} ) → ¬ (x == od∅ )→ Minimumo (od→ord x)
+         minord : (x : OD {suc n} ) → ¬ (x == od∅ ) → Minimumo (od→ord x)
          minord x not = ominimal (od→ord x) (∅9 not)
          minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 
          minimul x  not = ord→od ( mino (minord x not))
@@ -353,29 +363,16 @@
          omin→cmin  {x} {not} m<x = def-subst {suc n} {ord→od (od→ord x)} {od→ord (ord→od (mino (minord x not)))} (o<→c< m<x) oiso refl
          minimul<x : (x : OD {suc n} ) →  (not :  ¬ x == od∅ ) → x ∋ minimul x not
          minimul<x x not =  omin→cmin {x} {not} (min<x (minord x not)) 
-         omin∅≡min∅ : (ox : Ordinal {suc n}) → {not : ¬ ( ord→od ox == od∅)} 
-            → mino (ominimal ox (∅10 refl not)) ≡ mino (ominimal (od→ord (ord→od ox)) (∅9 not)) 
-         omin∅≡min∅ ox  {not} with ominimal ox (∅10 refl not)
-         omin∅≡min∅ record { lv = Zero ; ord = (Φ .0) }  | record { mino = mino ; min<x = case1 () }
-         omin∅≡min∅ record { lv = Zero ; ord = (Φ .0) }  | record { mino = mino ; min<x = case2 () }
-         omin∅≡min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) }  | record { mino = _ ; min<x = case1 () }
-         omin∅≡min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) }  | record { mino = record { lv = 0 ; ord = Φ 0 } ; min<x = case2 Φ< } =  {!!}
-         omin∅≡min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) } {_} | record { mino = record { lv = .0 ; ord = .(OSuc 0 _) } ; min<x = case2 (s< x)}  = {!!}
-         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) }  | record { mino = _ ; min<x = case1 (s≤s z≤n) } = {!!}
-         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) }  | record { mino = mino ; min<x = case2 () }
-         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) }  | record { mino = _ ; min<x = case1 (s≤s z≤n) } = {!!}
-         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) }  | record { mino = _ ; min<x = case2 lt } = {!!}
-         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) }  | record { mino = _ ; min<x = case1 (s≤s z≤n) } = {!!}
-         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = (ℵ .lv₁) }  | record { mino = _ ; min<x = case2 lt }  = {!!}
-         omin∅≡min∅ record { lv = (Suc lv₁) ; ord = ord } {not} | record { mino = mino ; min<x = min<x } = {!!}
-         omin∅→min∅ : (ox : Ordinal {suc n}) { x : OD {suc n} } →  {not : ¬ ( ord→od ox == od∅)} 
+         omin∅→min∅ : (ox : Ordinal {suc n})  →  {not : ¬ ( ord→od ox == od∅)} 
             → mino (ominimal ox (∅10 refl not)) ≡ o∅ → mino (ominimal (od→ord (ord→od ox)) (∅9 not)) ≡ o∅
-         omin∅→min∅ ox {x} {not} eq with ominimal ox (∅10 refl not)
+         omin∅→min∅ ox  {not} eq with ominimal ox (∅10 refl not)
          omin∅→min∅ record { lv = Zero ; ord = (Φ .0) }  eq | record { mino = mino ; min<x = case1 () }
          omin∅→min∅ record { lv = Zero ; ord = (Φ .0) }  eq | record { mino = mino ; min<x = case2 () }
          omin∅→min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) }  refl | record { mino = .o∅ ; min<x = case1 () }
-         omin∅→min∅ record { lv = Zero ; ord = (OSuc .0 ord₁) }  refl | record { mino = .o∅ ; min<x = case2 Φ< } = 
-               subst (λ k → ?  ≡ k  ) ? (omin∅→min∅ o∅ {!!})
+         omin∅→min∅ record { lv = Zero ; ord = (OSuc .0 (Φ .0)) } {not} refl | record { mino = record { lv = .0 ; ord = .(Φ 0) } ; min<x = case2 Φ< } = {!!}  where
+            lemma : mino (ominimal (od→ord (ord→od (record { lv = Zero ; ord = OSuc Zero (Φ Zero) }))) (∅5 (λ eq → not (∅7 eq)))) ≡ o∅
+            lemma = {!!}
+         omin∅→min∅ record { lv = Zero ; ord = (OSuc .0 (OSuc .0 ord₁)) } {_} refl | record { mino = record { lv = .0 ; ord = .(Φ 0) } ; min<x = case2 Φ< } = {!!}
          omin∅→min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) }  refl | record { mino = .o∅ ; min<x = case1 (s≤s z≤n) } = {!!}
          omin∅→min∅ record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) }  eq | record { mino = mino ; min<x = case2 () }
          omin∅→min∅ record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) }  refl | record { mino = .o∅ ; min<x = case1 (s≤s z≤n) } = {!!}
diff -r 87df00599a0e -r 164ad5a703d8 zf.agda
--- a/zf.agda	Wed May 29 18:50:57 2019 +0900
+++ b/zf.agda	Thu May 30 01:02:47 2019 +0900
@@ -68,8 +68,8 @@
      -- 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 
-     -- extentionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
-     extentionality :  ( A B z  : ZFSet  ) → (( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B
+     -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
+     extensionality :  ( A B 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  ≈ ∅ ) )