# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1558366201 -32400
# Node ID 3b0fdb95618e759e170023736d70e5e4877d63d7
# Parent  fce60b99dc55a12bb0da6e7fa52b21ada9aa2ab2
problem on Ordinal ( OSuc ℵ )

diff -r fce60b99dc55 -r 3b0fdb95618e ordinal-definable.agda
--- a/ordinal-definable.agda	Mon May 20 18:18:43 2019 +0900
+++ b/ordinal-definable.agda	Tue May 21 00:30:01 2019 +0900
@@ -77,6 +77,31 @@
 ∅1 : {n : Level} →  ( x : OD {n} )  → ¬ ( x c< od∅ {n} )
 ∅1 {n} x (lift ())
 
+∅3 : {n : Level} →  ( x : Ordinal {n})  → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n}
+∅3 {n} x = TransFinite {n} c1 c2 c3 x where
+   c0 : Nat →  Ordinal {n}  → Set n
+   c0 lx x = (∀(y : Ordinal {n}) → ¬ (y o< x))  → x ≡ o∅ {n}
+   c1 : ∀ (lx : Nat ) →  c0 lx (record { lv = Suc lx ; ord = ℵ lx } )  
+   c1 lx not with not ( record { lv = lx ; ord = Φ lx } )
+   ... | t with t (case1 ≤-refl )
+   c1 lx not | t | ()
+   c2 : (lx : Nat) → c0 lx (record { lv = lx ; ord = Φ lx } )
+   c2 Zero not = refl
+   c2 (Suc lx) not with not ( record { lv = lx ; ord = Φ lx } )
+   ... | t with t (case1 ≤-refl )
+   c2 (Suc lx) not | t | ()
+   c3 : (lx : Nat) (x₁ : OrdinalD lx) → c0 lx  (record { lv = lx ; ord = x₁ })  → c0 lx (record { lv = lx ; ord = OSuc lx x₁ })
+   c3 lx (Φ .lx) d not with not ( record { lv = lx ; ord = Φ lx } )
+   ... | t with t (case2 Φ< )
+   c3 lx (Φ .lx) d not | t | ()
+   c3 lx (OSuc .lx x₁) d not with not (  record { lv = lx ; ord = OSuc lx x₁ } )
+   ... | t with t (case2 (s< {!!} ) )
+   c3 lx (OSuc .lx x₁) d not | t | ()
+   c3 .(Suc lv) (ℵ lv) not = {!!}
+
+∅2 : {n : Level} →  od→ord ( od∅ {n} ) ≡ o∅ {n}
+∅2 {n}  = {!!}
+
 HOD→ZF : {n : Level} → ZF {suc n} {suc n}
 HOD→ZF {n}  = record { 
     ZFSet = OD {n}
@@ -126,7 +151,7 @@
        ;   power→ = {!!}
        ;   power← = {!!}
        ;   extentionality = {!!}
-       ;   minimul = {!!}
+       ;   minimul = minimul
        ;   regularity = {!!}
        ;   infinity∅ = {!!}
        ;   infinity = {!!}
@@ -143,9 +168,17 @@
          union→ X x y (lift X∋x) (lift x∋y) = lift lemma  where
             lemma : {z : Ordinal {n} } → def X z → z ≡ od→ord y
             lemma {z} X∋z = {!!}
-
-
-
-
-
-
+         -- _∋_ {n} a x  = def a ( od→ord x )
+         ¬∅ : (x : OD {n} ) → ¬ x ≡ od∅ → Ordinal {n}
+         ¬∅ = {!!}
+         ¬∅∈ : (x : OD {n} ) → (not : ¬ x ≡ od∅ ) → x ∋ (ord→od (¬∅ x not))
+         ¬∅∈ = {!!}
+         minimul : OD {n} → ( OD {n} ∧ OD {n} )
+         minimul x = {!!}
+         regularity : (x : OD) → ¬ x ≡ od∅ →
+                Lift (suc n) (x ∋ proj1 (minimul x)) ∧
+                (Select (proj1 (minimul x ) , x) (λ x₁ → Lift (suc n) (proj1 ( minimul x ) ∋ x₁) ∧ Lift (suc n) (x ∋ x₁)) ≡ od∅)
+         proj1 ( regularity x non ) = lift lemma where
+            lemma : def x (od→ord (proj1 (minimul x)))
+            lemma = {!!}
+         proj2 ( regularity x non ) = {!!}
diff -r fce60b99dc55 -r 3b0fdb95618e ordinal.agda
--- a/ordinal.agda	Mon May 20 18:18:43 2019 +0900
+++ b/ordinal.agda	Tue May 21 00:30:01 2019 +0900
@@ -30,11 +30,22 @@
 
 open import Data.Nat.Properties 
 open import Data.Empty
+open import Data.Unit using ( ⊤ )
 open import Relation.Nullary
 
 open import Relation.Binary
 open import Relation.Binary.Core
 
+¬ℵ : {n : Level} {lx : Nat } ( x : OrdinalD {n} lx ) → Set 
+¬ℵ (Φ lv₁) = ⊤
+¬ℵ (OSuc lv₁ x) = ¬ℵ x
+¬ℵ (ℵ lv₁) = ⊥
+
+s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → ¬ℵ x  → x d< OSuc lx x
+s<refl {n} {.lv₁} {Φ lv₁} t = Φ<
+s<refl {n} {.lv₁} {OSuc lv₁ x} t = s< (s<refl t)
+s<refl {n} {.(Suc lv₁)} {ℵ lv₁} ()
+
 o∅ : {n : Level} → Ordinal {n}
 o∅  = record { lv = Zero ; ord = Φ Zero }
 
@@ -167,13 +178,13 @@
      }
  }
 
-TransFinite : {n : Level} → ( ψ : Ordinal {n} → Set n ) 
+TransFinite : {n : Level} → { ψ : Ordinal {n} → Set n }
   → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } )) 
   → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
   → ( ∀ (lx : Nat ) → (x : OrdinalD lx )  → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
   →  ∀ (x : Ordinal)  → ψ x
-TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv } = caseΦ lv
-TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ } = caseOSuc lv ord₁
-    ( TransFinite ψ caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
-TransFinite ψ caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁
+TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv } = caseΦ lv
+TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ } = caseOSuc lv ord₁
+    ( TransFinite caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
+TransFinite caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁
 
diff -r fce60b99dc55 -r 3b0fdb95618e zf.agda
--- a/zf.agda	Mon May 20 18:18:43 2019 +0900
+++ b/zf.agda	Tue May 21 00:30:01 2019 +0900
@@ -80,8 +80,8 @@
      -- extentionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
      extentionality :  ( A B z  : ZFSet  ) → (( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B
      -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
-     minimul : ZFSet → ZFSet
-     regularity : ∀( x : ZFSet  ) → ¬ (x ≈ ∅) → (  minimul x ∈ x ∧  ( minimul x  ∩ x  ≈ ∅ ) )
+     minimul : ZFSet → ( ZFSet ∧ ZFSet )
+     regularity : ∀( x : ZFSet  ) → ¬ (x ≈ ∅) → ( proj1 ( minimul x ) ∈ x ∧  ( proj1 ( minimul x )  ∩ x  ≈ ∅ ) )
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
      infinity∅ :  ∅ ∈ infinite
      infinity :  ∀( X x : ZFSet  ) → x ∈ infinite →  ( x ∪ Select X (  λ y → x ≈ y )) ∈ infinite