--- a/ordinal-definable.agda	Thu May 23 14:20:35 2019 +0900
+++ b/ordinal-definable.agda	Thu May 23 19:48:51 2019 +0900
@@ -115,7 +115,7 @@
 ∅5 {n} record { lv = Zero ; ord = (OSuc .0 ord) } not = case2 Φ<
 ∅5 {n} record { lv = (Suc lv) ; ord = ord } not = case1 (s≤s z≤n)
 
--- postulate extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
+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
@@ -126,16 +126,60 @@
 ∅6 {n} x lt refl | tri≈ ¬a b ¬c =  ¬a lt
 ∅6 {n} x lt refl | tri> ¬a ¬b c = ¬b refl
 
+∅8 : {n : Level} →  ( x : Ordinal {n} )  → ¬  x o< o∅ {n}
+∅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 = {!!}
+
+open Ordinal
+
+
+∅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 ) {!!} {!!} )
+
+∅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 : Level} →  ( x : OD {n} )   → od→ord x ≡ o∅ {n} →  x  ≡ od∅ {n}
-∅7 = {!!}
+∅7 {n} x eq = trans ( trans (sym oiso)( cong ( λ k → ord→od k ) eq )  )  ∅7' 
 
 ∅9 : {n : Level} → (x : OD {n} ) → ¬ x ≡ od∅ → o∅ o< od→ord x
 ∅9 x not = ∅5 ( od→ord x) lemma where
    lemma : ¬ od→ord x ≡ o∅
    lemma eq = not ( ∅7 x eq )
 
-open Ordinal
-
 HOD→ZF : {n : Level} → ZF {suc n} {suc n}
 HOD→ZF {n}  = record { 
     ZFSet = OD {n}

--- a/ordinal.agda	Thu May 23 14:20:35 2019 +0900
+++ b/ordinal.agda	Thu May 23 19:48:51 2019 +0900
@@ -51,6 +51,11 @@
 s<refl {n} {lv} {OSuc lv x}  = s< s<refl 
 s<refl {n} {Suc lv} {ℵ lv} = ℵs<
 
+open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
+
+ordinal-cong : {n : Level} {x y : Ordinal {n}}  →
+      lv x  ≡ lv y → ord x ≅ ord y →  x ≡ y
+ordinal-cong refl refl = refl
 
 ≡→¬d< : {n : Level} →  {lv : Nat} → {x  : OrdinalD {n}  lv }  → x d< x → ⊥
 ≡→¬d<  {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t