--- 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 ) = {!!}