--- a/ordinal-definable.agda	Mon Jun 03 10:50:03 2019 +0900
+++ b/ordinal-definable.agda	Mon Jun 03 12:29:33 2019 +0900
@@ -68,13 +68,6 @@
   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 ψ
-  ∅-base-def : {n : Level} → def ( ord→od (o∅ {n}) ) ≡ def (od∅ {n})
-
-congf : {n : Level} {x y : OD {n}} → { f g : OD {n} → OD {n} } → x ≡ y → f ≡ g → f x ≡ g y 
-congf refl refl = refl
-
-o∅→od∅ : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n}
-o∅→od∅ {n} = cong ( λ k → record { def = k }) ( ∅-base-def ) 
 
 ∅1 : {n : Level} →  ( x : OD {n} )  → ¬ ( x c< od∅ {n} )
 ∅1 {n} x (lift ())
@@ -189,6 +182,27 @@
 ==→o≡ {n} {x} {y} eq | tri≈ ¬a b ¬c = b
 ==→o≡ {n} {x} {y} eq | tri> ¬a ¬b c = ⊥-elim ( o<→o> (eq-sym eq) (o<-subst c (sym ord-iso) (sym ord-iso )))
 
+¬x<0 : {n : Level} →  { x  : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} )
+¬x<0 {n} {x} (case1 ())
+¬x<0 {n} {x} (case2 ())
+
+-- o∅≡od∅0 : {n : Level} → ord→od (o∅ {suc n}) == od∅ {suc n}
+-- eq→ (o∅≡od∅0 {n} ) {x} y with c<→o< {suc n} {ord→od x} {ord→od (o∅ {suc n})} (def-subst {suc n} {_} {_} {ord→od o∅} {od→ord (ord→od x)} y refl (sym diso) )
+-- eq→ (o∅≡od∅0 {n}) {x} y | lt = ⊥-elim ( ¬x<0 (o<-subst lt  ord-iso  diso ) )
+-- eq← (o∅≡od∅0 {n}) {x} (lift ())
+-- 
+-- o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}
+-- o∅≡od∅ {n} = trans (cong (λ k → ord→od k ) ( ==→o≡ {n} (eq-trans o∅≡od∅0 (subst (λ k →  od∅ == k ) (sym oiso) eq-refl )) ) ) oiso
+
+o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}
+o∅≡od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (od∅ {suc n} ))
+o∅≡od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where
+    lemma :  o∅ {suc n } o< (od→ord (od∅ {suc n} )) → ⊥
+    lemma lt with def-subst (o<→c< lt) oiso refl
+    lemma lt | lift ()
+o∅≡od∅ {n} | tri≈ ¬a b ¬c = trans (cong (λ k → ord→od k ) b ) oiso
+o∅≡od∅ {n} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
+
 o<→¬== : {n : Level} →  { x y : OD {n} } → (od→ord x ) o< ( od→ord y) →  ¬ (x == y )
 o<→¬== {n} {x} {y} lt eq = o<→o> eq lt
 
@@ -239,9 +253,9 @@
      lemma ox ne with is-o∅ ox
      lemma ox ne | yes refl with ne ( ord→== lemma1 ) where
          lemma1 : od→ord (ord→od o∅) ≡ od→ord od∅
-         lemma1 = cong ( λ k → od→ord k ) o∅→od∅
+         lemma1 = cong ( λ k → od→ord k ) o∅≡od∅
      lemma o∅ ne | yes refl | ()
-     lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅→od∅ (o<→c< (∅5 ¬p))  
+     lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅≡od∅ (o<→c< (∅5 ¬p))  
 
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
@@ -360,7 +374,7 @@
          infinite = ord→od ( record { lv = Suc Zero ; ord = ℵ Zero  } )
          infinity∅ : ord→od ( record { lv = Suc Zero ; ord = ℵ Zero  } ) ∋ od∅ {suc n}
          infinity∅ = def-subst {suc n} {_} {od→ord (ord→od o∅)} {infinite} {od→ord od∅}
-              (o<→c< ( case1 (s≤s z≤n )))  refl (cong (λ k →  od→ord k) o∅→od∅ )
+              (o<→c< ( case1 (s≤s z≤n )))  refl (cong (λ k →  od→ord k) o∅≡od∅ )
          infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
          infinity x ∞∋x = {!!}
          replacement : {ψ : OD → OD} (X x : OD) → Replace X ψ ∋ ψ x