--- a/ordinal-definable.agda	Sat May 25 04:58:38 2019 +0900
+++ b/ordinal-definable.agda	Sat May 25 09:09:40 2019 +0900
@@ -64,6 +64,7 @@
 od∅ : {n : Level} → OD {n} 
 od∅ {n} = record { def = λ _ → Lift n ⊥ }
 
+open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
 
 postulate      
   c<→o< : {n : Level} {x y : OD {n} } → x c< y → od→ord x o< od→ord y
@@ -73,6 +74,14 @@
   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 ψ
   ∅-base-def : {n : Level} → def ( ord→od (o∅ {n}) ) ≡ def (od∅ {n})
+  ∅-base-lv : {n : Level} → lv ( od→ord (od∅ {n}) ) ≡ lv (o∅ {n})
+  ∅-base-d : {n : Level} → ord ( od→ord (od∅ {n}) ) ≅ ord (o∅ {n})
+
+o∅→od∅ : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n}
+o∅→od∅ {n} = cong ( λ k → record { def = k }) ( ∅-base-def ) 
+
+od∅→o∅ : {n : Level} →  od→ord (od∅ {n} ) ≡ o∅ {n} 
+od∅→o∅  = ordinal-cong ∅-base-lv ∅-base-d
 
 ∅1 : {n : Level} →  ( x : OD {n} )  → ¬ ( x c< od∅ {n} )
 ∅1 {n} x (lift ())
@@ -115,19 +124,6 @@
    lemma0 :  def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x ))) →  def z (od→ord x)
    lemma0 dz  = def-subst {n} { ord→od ( od→ord z )} { od→ord ( ord→od ( od→ord x))} dz (oiso) (diso)
 
-od∅' : {n : Level} → OD {n} 
-od∅' {n} = ord→od (o∅ {n}) 
-
-∅1' : {n : Level} →  ( x : OD {n} )  → ¬ ( x c< od∅' {n} )
-∅1' {n} x xc<o with  c<→o< {n} {x} {ord→od (o∅ {n})}  xc<o
-∅1' {n} x xc<o | case1 x₁ = {!!}
-∅1' {n} x xc<o | case2 x₁ = {!!}
- where
-   lemma : ( ox : Ordinal {n} ) → ox o< o∅ {n} → ⊥
-   lemma ox (case1 ())
-   lemma ox (case2 ())
-
-
 record Minimumo {n : Level } (x : Ordinal {n}) : Set (suc n) where
   field
      mino : Ordinal {n}
@@ -172,29 +168,29 @@
 -- ∅10 : {n : Level} → (x : OD {n} ) → ¬ ( ( y : OD {n} ) → Lift (suc n) ( x ∋ y))   →  x ≡ od∅ 
 -- ∅10 {n} x not = ?
 
--- ∋-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 = {!!} where
 
-∅7' : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n}
-∅7' {n} = cong ( λ k → record { def = k }) ( ∅-base-def ) 
+∅7' : {n : Level} → ord→od (o∅ {n}) == od∅ {n} 
+∅7' {n} = record { eq→ = e1 ;  eq← = e2 } where
+   e2 : {y : Ordinal {n}} → def od∅ y → def (ord→od (o∅ {n})) y 
+   e2 {y} (lift ())
+   e1 : {x : Ordinal {n} } → def (ord→od (o∅ {n})) x → def (od∅ {n})  x
+   e1 {x} o<x = def-subst {n} {ord→od (o∅ {n})} {x} o<x (cong (λ k → record { def = k }) ∅-base-def ) refl
 
-open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
+ord-iso : {n : Level} {y : Ordinal {n} } → record { lv = lv (od→ord (ord→od y)) ; ord = ord (od→ord (ord→od y)) } ≡ record { lv = lv y ; ord = ord y }
+ord-iso = cong ( λ k → record { lv = lv k ; ord = ord k } ) diso
 
 
-∅7 : {n : Level} →  ( x : OD {n} )   → od→ord x ≡ o∅ {n} →  x  == od∅ {n}
-∅7 {n} x eq = record { eq→ = e1 ; eq← = e2 } where
-   e0 : {y : Ordinal {n}} → y o< o∅ {n} → def od∅ y
-   e0 {y} (case1 ())
-   e0 {y} (case2 ())
-   e1 : {y : Ordinal {n}} →  def x y → def od∅ y
-   e1 {y} y<x  with  c<→o< {n} {x} y<x 
-   e1 {y} y<x | case1 lt = {!!}
-   e1 {y} y<x | case2 lt = {!!}
+∅7 : {n : Level} →  ( x : OD {n} ) → od→ord x ≡ o∅ {n} →  x  == od∅ {n}
+∅7 {n} x eq = record { eq→ = e1 eq ; eq← = e2 } where
    e2 : {y : Ordinal {n}} → def od∅ y → def x y 
    e2 {y} (lift ())
+   e1 : {ox y : Ordinal {n}} → ox ≡ o∅ {n}  →  def x y → def od∅ y
+   e1 {ox} {y} eq x>y with lv ox
+   e1 {o∅} {y} refl x>y | Zero   = lift ( ∅8 y (o<-subst (c<→o< {n} {ord→od y} {x} (def-subst {n} {x} {y} x>y refl (sym diso))) ord-iso eq ))  
+   e1 {o∅} {y} refl x>y | Suc lx = lift ( ∅8 y (o<-subst (c<→o< {n} {ord→od y} {x} (def-subst {n} {x} {y} x>y refl (sym diso))) ord-iso eq ))  
+
 
 open _∧_
 

--- a/ordinal.agda	Sat May 25 04:58:38 2019 +0900
+++ b/ordinal.agda	Sat May 25 09:09:40 2019 +0900
@@ -60,6 +60,12 @@
       lv x  ≡ lv y → ord x ≅ ord y →  x ≡ y
 ordinal-cong refl refl = refl
 
+ordinal-lv : {n : Level} {x y : Ordinal {n}}  → x ≡ y → lv x  ≡ lv y 
+ordinal-lv refl = refl
+
+ordinal-d : {n : Level} {x y : Ordinal {n}}  → x ≡ y → ord x  ≅ ord y 
+ordinal-d refl = refl
+
 ≡→¬d< : {n : Level} →  {lv : Nat} → {x  : OrdinalD {n}  lv }  → x d< x → ⊥
 ≡→¬d<  {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t