# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1558727918 -32400
# Node ID 33860eb44e4783f2754abf4825908fd02c3c7c28
# Parent  fcac01485f3296e9e98a8aa011b6b38e9e320df5
od∅' {n} = ord→od (o∅ {n})
 does not work

diff -r fcac01485f32 -r 33860eb44e47 ordinal-definable.agda
--- a/ordinal-definable.agda	Sat May 25 04:12:30 2019 +0900
+++ b/ordinal-definable.agda	Sat May 25 04:58:38 2019 +0900
@@ -27,13 +27,9 @@
 open Ordinal
 
 postulate      
-  od→lv : {n : Level} → OD {n} → Nat 
-  od→d : {n : Level} → (x : OD {n}) → OrdinalD {n} (od→lv x )
+  od→ord : {n : Level} → OD {n} → Ordinal {n}
   ord→od : {n : Level} → Ordinal {n} → OD {n} 
 
-od→ord : {n : Level} → OD {n} → Ordinal {n}
-od→ord x = record  { lv = od→lv x ; ord = od→d x }
-
 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n
 _∋_ {n} a x  = def a ( od→ord x )
 
@@ -68,6 +64,7 @@
 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
@@ -118,6 +115,19 @@
    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}
@@ -169,14 +179,11 @@
 -- ∅77 {n} x lt = {!!} where
 
 ∅7' : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n}
-∅7' {n} = cong ( λ k → record { def = k }) ( ∅-base-def ) where
+∅7' {n} = cong ( λ k → record { def = k }) ( ∅-base-def ) 
 
 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
 
 
-∅7'' : {n : Level} →  ( x : OD {n} )   → od→lv {n} x ≡ Zero → od→d {n} x ≅  Φ {n} Zero →  x  == od∅ {n}
-∅7'' {n} x eq eq1 = {!!}
-
 ∅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
@@ -189,6 +196,8 @@
    e2 : {y : Ordinal {n}} → def od∅ y → def x y 
    e2 {y} (lift ())
 
+open _∧_
+
 ∅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∅