--- a/ordinal-definable.agda	Thu May 23 19:48:51 2019 +0900
+++ b/ordinal-definable.agda	Thu May 23 20:24:15 2019 +0900
@@ -37,6 +37,9 @@
 _c≤_ : {n : Level} →  OD {n} →  OD {n} → Set (suc n)
 a c≤ b  = (a ≡ b)  ∨ ( b ∋ a )
 
+od∅ : {n : Level} → OD {n} 
+od∅ {n} = record { def = λ _ → Lift n ⊥ }
+
 postulate      
   c<→o< : {n : Level} {x y : OD {n} } → x c< y → od→ord x o< od→ord y
   o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → ord→od x c< ord→od y
@@ -44,11 +47,7 @@
   diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
   sup-od : {n : Level } → ( OD {n} → OD {n}) →  OD {n}
   sup-c< : {n : Level } → ( ψ : OD {n} →  OD {n}) → ∀ {x : OD {n}} → ψ x  c< sup-od ψ
-
-HOD = OD
-
-od∅ : {n : Level} → HOD {n} 
-od∅ {n} = record { def = λ _ → Lift n ⊥ }
+  ∅-base-def : {n : Level} → def ( ord→od (o∅ {n}) ) ≡ def (od∅ {n})
 
 ∅1 : {n : Level} →  ( x : OD {n} )  → ¬ ( x c< od∅ {n} )
 ∅1 {n} x (lift ())
@@ -117,9 +116,6 @@
 
 postulate extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
 
--- ∅7 : {n : Level} →  { x : OD {n} } → ((z :  OD {n}) → ¬ ( z c< x ))  → x ≡ od∅
--- ∅7 {n} {x} not = cong ( λ k → record { def = k } ) lemma2 where
-
 ∅6 : {n : Level } ( x : Ordinal {suc n}) → o∅ o< x → ¬ x ≡ o∅
 ∅6 {n} x lt eq with trio< {n} (o∅ {suc n}) x
 ∅6 {n} x lt refl | tri< a ¬b ¬c = ¬b refl
@@ -130,47 +126,19 @@
 ∅8 {n} x (case1 ())
 ∅8 {n} x (case2 ())
 
-∅7'' : {n : Level} → o∅ {suc n} ≡ od→ord (od∅ {suc n})
-∅7'' {n} = sym ( ∅3 lemma )  where
-   ⊥-leq : lift {_} {n} ⊥ ≡ lift {_} {n} ⊥
-   ⊥-leq = refl
-   lemma : {n : Level}  (y : Ordinal {suc n}) → ¬ (y o< od→ord od∅)
-   lemma {n} y lt = {!!}
-   -- with ⊥-leq 
-   -- ... | refl = ⊥-elim {!!} --- ∅1 (ord→od y) ( def-subst {suc n} {od∅} {y} {!!} {!!} {!!} )
-
-∅10 : {n : Level} → (x : OD {n} ) → ¬ ( ( y : OD {n} ) → Lift (suc n) ( x ∋ y))   →  x ≡ od∅ 
-∅10 {n} x not = cong ( λ k → record { def = k })  ( extensionality {n} ( λ y → {!!} ) ) where
-   ⊥-leq : lift {_} {n} ⊥ ≡ lift {_} {n} ⊥
-   ⊥-leq = refl
-   lemma : (y : Ordinal {n} ) → def x y ≡ def od∅ y
-   lemma y with def x y | def od∅ y
-   ... | s | t = {!!}
+-- ∅10 : {n : Level} → (x : OD {n} ) → ¬ ( ( y : OD {n} ) → Lift (suc n) ( x ∋ y))   →  x ≡ od∅ 
+-- ∅10 {n} x not = ?
 
 open Ordinal
 
+∋-subst : {n : Level} {X Y x y : OD {suc n} } → X ≡ x → Y ≡ y → X ∋ Y →  x ∋ y
+∋-subst refl refl x = x
 
-∅77 : {n : Level} → (x : OD {suc n} ) →  ¬ ( ord→od (o∅ {suc n}) ∋ x )
-∅77 {n} x lt with  od→ord x | c<→o< {suc n} {x} {ord→od (o∅ {suc n})} lt 
-... | s | t = lemma0 s t where
-   lemma : ( ox : Ordinal {suc n} ) → ox o< o∅ {suc n} → ⊥
-   lemma = ∅8
-   lemma1 : { y : Ordinal {suc n} } { la lA : Nat } { oa : OrdinalD {suc n} la }{ oA : OrdinalD {suc n} lA }
-       → ( record {lv = la ; ord = oa }  ≡  record {lv = lA ; ord = oA } )
-       → (la < lv y )  ∨ ( oa d< ord y ) →  (lA < lv y )  ∨ ( oA d< ord y )
-   lemma1 refl x = x
-   lemma0 : ( ox : Ordinal {suc n} ) →  ox o< od→ord (ord→od (o∅ {suc n}))  → ⊥
-   lemma0 = {!!}
-
---    lemma0 ox t = lemma ox ( lemma1 (diso {suc n} {o∅ {suc n}}) t )
---- ... | s | t = lemma s t (diso {suc n} {o∅ {suc n}}) where
--- with od→ord x |  c<→o< {n} {x} {ord→od (o∅ {n})} lt
--- ∅8 {n} (od→ord x) ( def-subst {n} {ord→od (od→ord x) } {{!!}} ( c<→o< lt ) {!!} {!!} )
+-- ∅77 : {n : Level} → (x : OD {suc n} ) →  ¬ ( ord→od (o∅ {suc n}) ∋ x )
+-- ∅77 {n} x lt = {!!} where
 
 ∅7' : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n}
-∅7' {n} = cong ( λ k → record { def = k }) ( extensionality {n} lemma ) where
-   lemma : ( x : Ordinal {n} )  →   def (ord→od o∅) x ≡ def od∅ x
-   lemma x = {!!}
+∅7' {n} = cong ( λ k → record { def = k }) ( ∅-base-def ) where
 
 ∅7 : {n : Level} →  ( x : OD {n} )   → od→ord x ≡ o∅ {n} →  x  ≡ od∅ {n}
 ∅7 {n} x eq = trans ( trans (sym oiso)( cong ( λ k → ord→od k ) eq )  )  ∅7' 
@@ -180,8 +148,8 @@
    lemma : ¬ od→ord x ≡ o∅
    lemma eq = not ( ∅7 x eq )
 
-HOD→ZF : {n : Level} → ZF {suc n} {suc n}
-HOD→ZF {n}  = record { 
+OD→ZF : {n : Level} → ZF {suc n} {suc n}
+OD→ZF {n}  = record { 
     ZFSet = OD {n}
     ; _∋_ = λ a x → Lift (suc n) ( a ∋ x )
     ; _≈_ = _≡_