# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1558725150 -32400
# Node ID fcac01485f3296e9e98a8aa011b6b38e9e320df5
# Parent  0d9b9db1436155f4a27a8fa6d2ad5ea1fb2ff26f
  od→lv : {n : Level} → OD {n} → Nat
does not worked

diff -r 0d9b9db14361 -r fcac01485f32 ordinal-definable.agda
--- a/ordinal-definable.agda	Fri May 24 22:22:16 2019 +0900
+++ b/ordinal-definable.agda	Sat May 25 04:12:30 2019 +0900
@@ -24,10 +24,16 @@
 open OD
 open import Data.Unit
 
+open Ordinal
+
 postulate      
-  od→ord : {n : Level} → OD {n} → Ordinal {n}
+  od→lv : {n : Level} → OD {n} → Nat 
+  od→d : {n : Level} → (x : OD {n}) → OrdinalD {n} (od→lv x )
   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 )
 
@@ -126,8 +132,8 @@
 ominimal {n} record { lv = (Suc lv) ; ord = (Φ .(Suc lv)) } (case2 ())
 ominimal {n} record { lv = (Suc lv) ; ord = (OSuc .(Suc lv) ord) } (case1 (s≤s x)) = record { mino = record { lv = (Suc lv) ; ord = ord } ; min<x = case2 s<refl}
 ominimal {n} record { lv = (Suc lv) ; ord = (OSuc .(Suc lv) ord) } (case2 ())
-ominimal {n} record { lv = (Suc lv) ; ord = (ℵ .lv) } (case1 (s≤s z≤n)) = record { mino = record { lv = Suc lv ; ord = Φ (Suc lv) } ; min<x = case2 ℵΦ<  }
-ominimal {n} record { lv = (Suc lv) ; ord = (ℵ .lv) } (case2 ())
+ominimal {n} record { lv = (Suc lx) ; ord = (ℵ .lx) } (case1 (s≤s z≤n)) = record { mino = record { lv = Suc lx ; ord = Φ (Suc lx) } ; min<x = case2 ℵΦ<  }
+ominimal {n} record { lv = (Suc lx) ; ord = (ℵ .lx) } (case2 ())
 
 ∅4 : {n : Level} →  ( x : OD {n} )  →  x  ≡ od∅ {n}  → od→ord x ≡ o∅ {n}
 ∅4 {n} x refl =  ∅3 lemma1 where
@@ -156,8 +162,6 @@
 -- ∅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
 
@@ -167,13 +171,21 @@
 ∅7' : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n}
 ∅7' {n} = cong ( λ k → record { def = k }) ( ∅-base-def ) where
 
+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
    e0 {y} (case1 ())
    e0 {y} (case2 ())
    e1 : {y : Ordinal {n}} →  def x y → def od∅ y
-   e1 {y} y<x = e0 ( o<-subst ( c<→o< {n} {x} y<x ) refl {!!} )
+   e1 {y} y<x  with  c<→o< {n} {x} y<x 
+   e1 {y} y<x | case1 lt = {!!}
+   e1 {y} y<x | case2 lt = {!!}
    e2 : {y : Ordinal {n}} → def od∅ y → def x y 
    e2 {y} (lift ())
 
@@ -182,6 +194,7 @@
    lemma : ¬ od→ord x ≡ o∅
    lemma eq = not ( ∅7 x eq )
 
+
 OD→ZF : {n : Level} → ZF {suc n} {n}
 OD→ZF {n}  = record { 
     ZFSet = OD {n}