# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559577933 -32400
# Node ID 96c932d0145d4f25ac3bac10581f5d009d959384
# Parent  461690d60d078ca4fbc829ff60c712185fc778c3
simpler ordinal

diff -r 461690d60d07 -r 96c932d0145d ordinal-definable.agda
--- a/ordinal-definable.agda	Mon Jun 03 12:29:33 2019 +0900
+++ b/ordinal-definable.agda	Tue Jun 04 01:05:33 2019 +0900
@@ -73,13 +73,9 @@
 ∅1 {n} x (lift ())
 
 ∅3 : {n : Level} →  { x : Ordinal {n}}  → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n}
-∅3 {n} {x} = TransFinite {n} c1 c2 c3 x where
+∅3 {n} {x} = TransFinite {n} c2 c3 x where
    c0 : Nat →  Ordinal {n}  → Set n
    c0 lx x = (∀(y : Ordinal {n}) → ¬ (y o< x))  → x ≡ o∅ {n}
-   c1 : ∀ (lx : Nat ) →  c0 lx (record { lv = Suc lx ; ord = ℵ lx } )  
-   c1 lx not with not ( record { lv = lx ; ord = Φ lx } )
-   ... | t with t (case1 ≤-refl )
-   c1 lx not | t | ()
    c2 : (lx : Nat) → c0 lx (record { lv = lx ; ord = Φ lx } )
    c2 Zero not = refl
    c2 (Suc lx) not with not ( record { lv = lx ; ord = Φ lx } )
@@ -92,9 +88,6 @@
    c3 lx (OSuc .lx x₁) d not with not (  record { lv = lx ; ord = OSuc lx x₁ } )
    ... | t with t (case2 (s< s<refl ) )
    c3 lx (OSuc .lx x₁) d not | t | ()
-   c3 (Suc lx) (ℵ lx) d not with not ( record { lv = Suc lx ; ord = OSuc (Suc lx) (Φ (Suc lx)) }  )
-   ... | t with t (case2 (s< ℵΦ<   )) 
-   c3 .(Suc lx) (ℵ lx) d not | t | ()
 
 def-subst : {n : Level } {Z : OD {n}} {X : Ordinal {n} }{z : OD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
 def-subst df refl refl = df
@@ -153,15 +146,6 @@
 c≤-refl : {n : Level} →  ( x : OD {n} ) → x c≤ x
 c≤-refl x = case1 refl
 
-o<> : {n : Level } ( ox oy : Ordinal {n}) → ox o<  oy  → oy o< ox  →  ⊥
-o<> ox oy (case1 x<y) (case1 y<x) = >→¬< x<y y<x
-o<> ox oy (case1 x<y) (case2 y<x) with d<→lv  y<x
-... | refl = =→¬< x<y
-o<> ox oy (case2 x<y) (case1 y<x) with d<→lv  x<y
-... | refl = =→¬< y<x
-o<> ox oy (case2 x<y) (case2 y<x) with d<→lv  x<y
-... | refl = trio<> x<y y<x
-
 o<¬≡ : {n : Level } ( ox oy : Ordinal {n}) → ox ≡ oy  → ox o< oy  → ⊥
 o<¬≡ ox ox refl (case1 lt) =  =→¬< lt
 o<¬≡ ox ox refl (case2 (s< lt)) = trio<≡ refl lt
@@ -186,14 +170,6 @@
 ¬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
@@ -207,7 +183,7 @@
 o<→¬== {n} {x} {y} lt eq = o<→o> eq lt
 
 o<→¬c> : {n : Level} →  { x y : OD {n} } → (od→ord x ) o< ( od→ord y) →  ¬ (y c< x )
-o<→¬c> {n} {x} {y} olt clt = o<> (od→ord x) (od→ord y) olt (c<→o< clt ) where
+o<→¬c> {n} {x} {y} olt clt = o<> olt (c<→o< clt ) where
 
 o≡→¬c< : {n : Level} →  { x y : OD {n} } →  (od→ord x ) ≡ ( od→ord y) →   ¬ x c< y
 o≡→¬c< {n} {x} {y} oeq lt  = o<¬≡ (od→ord x) (od→ord y) (orefl oeq ) (c<→o< lt) 
@@ -270,7 +246,7 @@
     ; Power = Power
     ; Select = Select
     ; Replace = Replace
-    ; infinite = ord→od ( record { lv = Suc Zero ; ord = ℵ Zero  } )
+    ; infinite = ord→od ( record { lv = Suc Zero ; ord = Φ 1 } )
     ; isZF = isZF 
  } where
     Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n}
@@ -296,7 +272,7 @@
     infixr  200 _∈_
     infixr  230 _∩_ _∪_
     infixr  220 _⊆_
-    isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace (ord→od ( record { lv = Suc Zero ; ord = ℵ Zero  } ))
+    isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace (ord→od ( record { lv = Suc Zero ; ord = Φ 1} ))
     isZF = record {
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
        ;   pair  = pair
@@ -368,15 +344,23 @@
          eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
          eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d  
          next : (x : OD) → Union (x , (x , x)) == ord→od (osuc (od→ord x))
-         eq→ (next x ) {y} z = {!!}
+         eq→ (next x ) {y} z = {!!} 
          eq← (next x ) {y} z = {!!}
+         next' : (x : OD) →  ord→od ( od→ord ( Union (x , (x , x)))) == ord→od (osuc (od→ord x))
+         next' x = subst ( λ k → k == ord→od (osuc (od→ord x))) (sym oiso) (next x)
          infinite : OD {suc n}
-         infinite = ord→od ( record { lv = Suc Zero ; ord = ℵ Zero  } )
-         infinity∅ : ord→od ( record { lv = Suc Zero ; ord = ℵ Zero  } ) ∋ od∅ {suc n}
+         infinite = ord→od ( record { lv = Suc Zero ; ord = Φ 1 } )
+         infinity∅ : ord→od ( record { lv = Suc Zero ; ord = Φ 1  } ) ∋ 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∅ )
          infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
-         infinity x ∞∋x = {!!}
+         infinity x ∞∋x = {!!} where
+             lemma : (ox : Ordinal {suc n} ) → ox o< record { lv = Suc Zero ; ord = Φ 1 } → osuc ox o< record { lv = Suc Zero ; ord = Φ 1 } 
+             lemma record { lv = Zero ; ord = (Φ .0) } (case1 (s≤s x)) = case1 {!!}
+             lemma record { lv = Zero ; ord = (OSuc .0 ord₁) } (case1 (s≤s x)) = case1 {!!}
+             lemma record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } (case1 (s≤s ()))
+             lemma record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } (case1 (s≤s ()))
+             lemma record { lv = 1 ; ord = (Φ 1) } (case2 ℵΦ<) = case2 {!!}
          replacement : {ψ : OD → OD} (X x : OD) → Replace X ψ ∋ ψ x
          replacement {ψ} X x = {!!}
 
diff -r 461690d60d07 -r 96c932d0145d ordinal.agda
--- a/ordinal.agda	Mon Jun 03 12:29:33 2019 +0900
+++ b/ordinal.agda	Tue Jun 04 01:05:33 2019 +0900
@@ -11,27 +11,18 @@
 data OrdinalD {n : Level} :  (lv : Nat) → Set n where
    Φ : (lv : Nat) → OrdinalD  lv
    OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
-   ℵ_ :  (lv : Nat) → OrdinalD (Suc lv)
 
 record Ordinal {n : Level} : Set n where
    field
      lv : Nat
      ord : OrdinalD {n} lv
 
-data ¬ℵ  {n : Level} {lx : Nat } : ( x : OrdinalD {n} lx ) → Set where
-    ¬ℵΦ : ¬ℵ (Φ lx) 
-    ¬ℵs : {x : OrdinalD {n} lx } → ¬ℵ x → ¬ℵ (OSuc lx x) 
-
 --
 --    Φ (Suc lv) < ℵ lv < OSuc (Suc lv) (ℵ lv) < OSuc ... < OSuc (Suc lv) (Φ (Suc lv)) < OSuc ...  < ℵ (Suc lv)
 --
 data _d<_ {n : Level} :   {lx ly : Nat} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Set n where
    Φ<  : {lx : Nat} → {x : OrdinalD {n} lx}  →  Φ lx d< OSuc lx x
    s<  : {lx : Nat} → {x y : OrdinalD {n} lx}  →  x d< y  → OSuc  lx x d< OSuc  lx y
-   ℵΦ< : {lx : Nat} → Φ  (Suc lx) d< (ℵ lx) 
-   ℵ<  : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } → ¬ℵ x  →  OSuc  (Suc lx) x d< (ℵ lx) 
-   ℵs< : {lx : Nat} → (ℵ lx) d< OSuc (Suc lx) (ℵ lx)
-   ℵss< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } → (ℵ lx) d< x → (ℵ lx) d< OSuc (Suc lx) x 
 
 open Ordinal
 
@@ -41,26 +32,14 @@
 s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x
 s<refl {n} {lv} {Φ lv}  = Φ<
 s<refl {n} {lv} {OSuc lv x}  = s< s<refl 
-s<refl {n} {Suc lv} {ℵ lv} = ℵs<
 
 trio<> : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  →  y d< x → x d< y → ⊥
 trio<>  {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) = trio<> s t
-trio<> {_} {.(Suc _)} {.(OSuc (Suc _) (ℵ _))} {.(ℵ _)} ℵs< (ℵ< {_} {.(ℵ _)} ())
-trio<> {_} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (ℵ _))} (ℵ< ()) ℵs<
 trio<> {n} {lx} {.(OSuc lx _)} {.(Φ lx)} Φ< ()
-trio<> {n} {.(Suc _)} {.(ℵ _)} {.(Φ (Suc _))} ℵΦ< ()
-trio<> {n} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (Φ (Suc _)))} (ℵ< ¬ℵΦ) (ℵss< ())
-trio<> {n} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (OSuc (Suc _) _))} (ℵ< (¬ℵs x)) (ℵss< x<y) = trio<> (ℵ< x) x<y
-trio<> {n} {.(Suc _)} {.(OSuc (Suc _) (Φ (Suc _)))} {.(ℵ _)} (ℵss< ()) (ℵ< ¬ℵΦ)
-trio<> {n} {.(Suc _)} {.(OSuc (Suc _) (OSuc (Suc _) _))} {.(ℵ _)} (ℵss< y<x) (ℵ< (¬ℵs x)) = trio<> y<x (ℵ< x)
 
 d<→lv : {n : Level} {x y  : Ordinal {n}}   → ord x d< ord y → lv x ≡ lv y
 d<→lv Φ< = refl
 d<→lv (s< lt) = refl
-d<→lv ℵΦ< = refl
-d<→lv (ℵ< _) = refl
-d<→lv ℵs< = refl
-d<→lv (ℵss< _) = refl
 
 o<-subst : {n : Level } {Z X z x : Ordinal {n}}  → Z o< X → Z ≡ z  →  X ≡ x  →  z o< x
 o<-subst df refl refl = df
@@ -99,25 +78,10 @@
 triO : {n : Level} →  {lx ly : Nat} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Tri (lx < ly) ( lx ≡ ly ) ( lx > ly )
 triO  {n} {lx} {ly} x y = <-cmp lx ly
 
-fin : {n : Level} →  {lx : Nat} → {y : OrdinalD {n} (Suc lx) } → y d< (ℵ lx) → ¬ℵ y
-fin {_} {_} {Φ (Suc _)} ℵΦ< = ¬ℵΦ
-fin {_} {_} {OSuc (Suc _) _} (ℵ< x) = ¬ℵs x
-
 triOrdd : {n : Level} →  {lx : Nat}   → Trichotomous  _≡_ ( _d<_  {n} {lx} {lx} )
 triOrdd  {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d<
-triOrdd  {_} {Suc lv} (ℵ lv) (ℵ lv) = tri≈ ≡→¬d< refl ≡→¬d<
 triOrdd  {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< )
-triOrdd  {_} {.(Suc lv)} (Φ (Suc lv)) (ℵ lv) = tri<  ℵΦ<  (λ ()) ( λ lt → trio<> lt ℵΦ<) 
-triOrdd  {_} {Suc lv} (ℵ lv) (Φ (Suc lv)) = tri> ( λ lt → trio<> lt ℵΦ< ) (λ ()) ℵΦ<  
-triOrdd {_} {Suc lv} (ℵ lv) (OSuc (Suc lv) y ) with triOrdd (ℵ lv) y
-triOrdd {_} {Suc lv} (ℵ lv) (OSuc .(Suc lv) y) | tri< a ¬b ¬c = tri< (ℵss< a) (λ ()) (trio<> (ℵss< a) )
-triOrdd {_} {Suc lv} (ℵ lv) (OSuc .(Suc lv) y) | tri≈ ¬a refl ¬c = tri<  ℵs< (λ ()) ( λ lt → trio<> lt  ℵs< )
-triOrdd {_} {Suc lv} (ℵ lv) (OSuc .(Suc lv) y) | tri> ¬a ¬b c = tri> ( λ lt → trio<> lt ( ℵ< (fin c))  ) (λ ()) ( ℵ< (fin c) )
 triOrdd  {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ<
-triOrdd  {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) with triOrdd x (ℵ lv)
-triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) | tri< a ¬b ¬c = tri< (ℵ< (fin a ) ) (λ ()) (  λ lt → trio<> lt (ℵ< (fin a ))) 
-triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) | tri≈ ¬a refl ¬c = tri> (λ lt → trio<> lt ℵs< ) (λ ()) ℵs< 
-triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) | tri> ¬a ¬b c = tri> (λ lt → trio<> lt (ℵss< c  )) (λ ()) ( ℵss< c  )
 triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) with triOrdd x y
 triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) | tri< a ¬b ¬c = tri< (s< a) (λ tx=ty → trio<≡ tx=ty (s< a) )  (  λ lt → trio<> lt (s< a) )
 triOrdd  {_} {lv} (OSuc lv x) (OSuc lv x) | tri≈ ¬a refl ¬c = tri≈ ≡→¬d< refl ≡→¬d<
@@ -129,7 +93,6 @@
 <-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x
 <-osuc {n} {record { lv = lx ; ord = Φ .lx }} =  case2 Φ<
 <-osuc {n} {record { lv = lx ; ord = OSuc .lx ox }} = case2 ( s< s<refl )
-<-osuc {n} {record { lv = (Suc lx) ; ord = ℵ lx }} = case2 ℵs<
 
 osuc-lveq : {n : Level} { x : Ordinal {n} } → lv x ≡ lv ( osuc x )
 osuc-lveq {n} = refl
@@ -140,73 +103,43 @@
 nat-<≡ : { x : Nat } → x < x → ⊥
 nat-<≡  (s≤s lt) = nat-<≡ lt
 
+nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥
+nat-≡< refl lt = nat-<≡ lt
+
 ¬a≤a : {la : Nat} → Suc la ≤ la → ⊥
 ¬a≤a  (s≤s lt) = ¬a≤a  lt
 
-xsyℵ :  {n : Level} {lx : Nat} {x y : OrdinalD {n}  lx }   → x d< y → ¬ℵ y → ¬ℵ x
-xsyℵ {_} {_} {Φ lv₁} {y} x<y t = ¬ℵΦ
-xsyℵ {_} {_} {OSuc lv₁ x} {OSuc lv₁ y} (s< x<y) (¬ℵs t) = ¬ℵs ( xsyℵ x<y t)
-xsyℵ {_} {_} {OSuc .(Suc _) x} {.(ℵ _)} (ℵ< x₁) ()
-xsyℵ {_} {_} {ℵ lv₁} {.(OSuc (Suc lv₁) (ℵ lv₁))} ℵs< (¬ℵs t) = t
-xsyℵ (ℵss< ()) (¬ℵs ¬ℵΦ)
-xsyℵ (ℵss< x<y) (¬ℵs t) = xsyℵ x<y t
+o<> : {n : Level} →  {x y : Ordinal {n}  }  →  y o< x → x o< y → ⊥
+o<> {n} {x} {y} (case1 x₁) (case1 x₂) = nat-<>  x₁ x₂
+o<> {n} {x} {y} (case1 x₁) (case2 x₂) = nat-≡< (sym (d<→lv x₂)) x₁
+o<> {n} {x} {y} (case2 x₁) (case1 x₂) = nat-≡< (sym (d<→lv x₁)) x₂
+o<> {n} {record { lv = lv₁ ; ord = .(OSuc lv₁ _) }} {record { lv = .lv₁ ; ord = .(Φ lv₁) }} (case2 Φ<) (case2 ())
+o<> {n} {record { lv = lv₁ ; ord = .(OSuc lv₁ _) }} {record { lv = .lv₁ ; ord = .(OSuc lv₁ _) }} (case2 (s< y<x)) (case2 (s< x<y)) = 
+   o<> (case2 y<x) (case2 x<y)
 
 orddtrans : {n : Level} {lx : Nat} {x y z : OrdinalD {n}  lx }   → x d< y → y d< z → x d< z
 orddtrans {_} {lx} {.(Φ lx)} {.(OSuc lx _)} {.(OSuc lx _)} Φ< (s< y<z) = Φ< 
-orddtrans {_} {Suc lx} {Φ (Suc lx)} {OSuc (Suc lx) y} {ℵ lx} Φ< (ℵ< _) = ℵΦ< 
 orddtrans {_} {lx} {.(OSuc lx _)} {.(OSuc lx _)} {.(OSuc lx _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z )
-orddtrans {_} {Suc lx} {.(OSuc (Suc lx) _)} {.(OSuc (Suc lx) (Φ (Suc lx)))} {.(ℵ lx)} (s< ()) (ℵ< ¬ℵΦ)
-orddtrans ℵs< (ℵ< ())
-orddtrans {n} {Suc lx} {OSuc (Suc lx) x} {OSuc (Suc ly) y} {ℵ _} (s< x<y) (ℵ< t) = ℵ< ( xsyℵ x<y t )
-orddtrans {n} {.(Suc _)} {.(Φ (Suc _))} {.(ℵ _)} {.(OSuc (Suc _) (ℵ _))} ℵΦ< ℵs< = Φ<
-orddtrans {n} {.(Suc _)} {OSuc (Suc _) .(Φ (Suc _))} {.(ℵ _)} {OSuc (Suc _) (ℵ k)} (ℵ< ¬ℵΦ) ℵs< = s<  ℵΦ< 
-orddtrans {n} {.(Suc _)} {OSuc (Suc lv) (OSuc (Suc _) x)} {ℵ lv} {.(OSuc (Suc _) (ℵ _))} (ℵ< (¬ℵs t)) ℵs< = s< ( ℵ< t )
-orddtrans {n} {.(Suc lv)} {ℵ lv} {OSuc .(Suc lv) (ℵ lv)} {OSuc .(Suc lv) .(OSuc (Suc lv) (ℵ lv))} ℵs< (s< ℵs<) = ℵss< ℵs<
-orddtrans ℵΦ< (ℵss< y<z) = Φ<
-orddtrans (ℵ< {lx} {Φ .(Suc lx)} nxx) (ℵss< {_} {k} y<z) = s< (orddtrans ℵΦ<   y<z)
-orddtrans (ℵ< {lx} {OSuc .(Suc lx) xx} (¬ℵs nxx)) (ℵss< y<z) = s< (orddtrans (ℵ< nxx) y<z) 
-orddtrans (ℵ< {.lv₁} {ℵ lv₁} ()) (ℵss< y<z) 
-orddtrans (ℵss< x<y) (s< y<z) = ℵss< ( orddtrans x<y y<z )
-orddtrans (ℵss< ()) (ℵ< ¬ℵΦ)
-orddtrans (ℵss< ℵs<) (ℵ< (¬ℵs ()))
-orddtrans (ℵss< (ℵss< x<y)) (ℵ< (¬ℵs x)) = orddtrans (ℵss< x<y) ( ℵ< x )
-orddtrans {n} {Suc lx} {x} {y} {z} ℵs< (s< (ℵss< {lx} {ss} y<z)) = ℵss< ( ℵss< y<z )
 
 osuc-≡< : {n : Level} { a x : Ordinal {n} } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)  
 osuc-≡< {n} {a} {x} (case1 lt) = case2 (case1 lt)
 osuc-≡< {n} {record { lv = lv₁ ; ord = Φ .lv₁ }} {record { lv = .lv₁ ; ord = .(Φ lv₁) }} (case2 Φ<) = case1 refl
 osuc-≡< {n} {record { lv = lv₁ ; ord = OSuc .lv₁ ord₁ }} {record { lv = .lv₁ ; ord = .(Φ lv₁) }} (case2 Φ<) = case2 (case2 Φ<)
-osuc-≡< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = .(Suc lv₁) ; ord = .(Φ (Suc lv₁)) }} (case2 Φ<) = case2 (case2 ℵΦ<)
 osuc-≡< {n} {record { lv = lv₁ ; ord = Φ .lv₁ }} {record { lv = .lv₁ ; ord = .(OSuc lv₁ _) }} (case2 (s< ()))
 osuc-≡< {n} {record { lv = la ; ord = OSuc la oa }} {record { lv = la ; ord = (OSuc la ox) }} (case2 (s< lt)) with
       osuc-≡< {n} {record { lv = la ; ord = oa }} {record { lv = la ; ord = ox }} (case2 lt )
 ... | case1 refl = case1 refl
 ... | case2 (case2 x) = case2 (case2( s< x) )
 ... | case2 (case1 x) = ⊥-elim (¬a≤a  x) where
-osuc-≡< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = .(Suc lv₁) ; ord = .(OSuc (Suc lv₁) (Φ (Suc lv₁))) }} (case2 (s< ℵΦ<)) = case2 (case2 (ℵ< ¬ℵΦ ))
-osuc-≡< {n} {record { lv = (Suc lx) ; ord = ℵ lx }} {record { lv = (Suc lx) ; ord = (OSuc (Suc lx) (OSuc (Suc lx) ox)) }} (case2 (s< (ℵ< x))) with
-   osuc-≡< {n} {record { lv = (Suc lx) ; ord = ℵ lx }} {record { lv = (Suc lx) ; ord = (OSuc (Suc lx) ox) }} (case2 (lemma (ℵ< x)) ) where
-      lemma : OSuc (Suc lx) ox d< (ℵ lx) → OSuc (Suc lx) ox d< ord (osuc (record { lv = Suc lx ; ord = ℵ lx }))
-      lemma lt = orddtrans lt s<refl
-... | case1 ()
-... | case2 ttt = case2 ( case2 (ℵ< (¬ℵs x) ))
-osuc-≡< {n} {record { lv = .(Suc _) ; ord = .(ℵ _) }} {record { lv = .(Suc _) ; ord = .(ℵ _) }} (case2 ℵs<) = case1 refl
-osuc-≡< {n} {record { lv = .(Suc _) ; ord = Φ .(Suc _) }} {record { lv = .(Suc _) ; ord = .(ℵ _) }} (case2 (ℵss< lt)) = case2 (case2 lt)
-osuc-≡< {n} {record { lv = .(Suc _) ; ord = OSuc .(Suc _) ord₁ }} {record { lv = .(Suc _) ; ord = .(ℵ _) }} (case2 (ℵss< lt)) = case2 (case2 lt)
-osuc-≡< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = .(Suc lv₁) ; ord = .(ℵ lv₁) }} (case2 (ℵss< lt)) = case1 refl
 
 osuc-< : {n : Level} { x y : Ordinal {n} } → y o< osuc x  → x o< y → ⊥
 osuc-< {n} {x} {y} y<ox x<y with osuc-≡< y<ox
 osuc-< {n} {x} {x} y<ox (case1 x₁) | case1 refl = ⊥-elim (¬a≤a x₁)
 osuc-< {n} {x} {x} (case1 x₂) (case2 x₁) | case1 refl = ⊥-elim (¬a≤a x₂)
 osuc-< {n} {x} {x} (case2 x₂) (case2 x₁) | case1 refl = ≡→¬d<  x₁
-osuc-< {n} {x} {y} y<ox (case1 x₂) | case2 (case1 x₁) = nat-<> x₁ x₂
-osuc-< {n} {x} {y} y<ox (case2 x₂) | case2 (case1 x₁) with d<→lv x₂
-... | refl = ⊥-elim (¬a≤a x₁)
-osuc-< {n} {x} {y} y<ox (case1 x₁) | case2 (case2 y<x) with d<→lv y<x
-... | refl = ⊥-elim (¬a≤a x₁)
-osuc-< {n} {x} {y} y<ox (case2 x<y) | case2 (case2 y<x) with d<→lv y<x | d<→lv x<y
-... | refl | refl = trio<> y<x x<y
+osuc-< {n} {x} {y} y<ox (case1 x₂) | case2 (case1 x₁) = nat-<> x₂ x₁
+osuc-< {n} {x} {y} y<ox (case1 x₂) | case2 (case2 x₁) = nat-≡< (sym (d<→lv x₁)) x₂
+osuc-< {n} {x} {y} y<ox (case2 x<y) | case2 y<x = o<> (case2 x<y) y<x
 
 max : (x y : Nat) → Nat
 max Zero Zero = Zero
@@ -231,26 +164,23 @@
 
 ordtrans : {n : Level} {x y z : Ordinal {n} }   → x o< y → y o< z → x o< z
 ordtrans {n} {x} {y} {z} (case1 x₁) (case1 x₂) = case1 ( <-trans x₁ x₂ )
-ordtrans {n} {x} {y} {z} (case1 x₁) (case2 x₂) with d<→lv x₂
+ordtrans {n} {x} {y} {z} (case1 x₁) (case2 x₂) with  d<→lv x₂
 ... | refl = case1 x₁
-ordtrans {n} {x} {y} {z} (case2 x₁) (case1 x₂) with d<→lv x₁
+ordtrans {n} {x} {y} {z} (case2 x₁) (case1 x₂)  with  d<→lv x₁
 ... | refl = case1 x₂
 ordtrans {n} {x} {y} {z} (case2 x₁) (case2 x₂) with d<→lv x₁ | d<→lv x₂
 ... | refl | refl = case2 ( orddtrans x₁ x₂ )
 
-
 trio< : {n : Level } → Trichotomous {suc n} _≡_  _o<_ 
 trio< a b with <-cmp (lv a) (lv b)
 trio< a b | tri< a₁ ¬b ¬c = tri< (case1  a₁) (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) lemma1 where
    lemma1 : ¬ (Suc (lv b) ≤ lv a) ∨ (ord b d< ord a)
    lemma1 (case1 x) = ¬c x
-   lemma1 (case2 x) with d<→lv x
-   lemma1 (case2 x) | refl = ¬b refl
+   lemma1 (case2 x) = ⊥-elim (nat-≡< (sym ( d<→lv x )) a₁  )
 trio< a b | tri> ¬a ¬b c = tri> lemma1 (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) (case1 c) where
    lemma1 : ¬ (Suc (lv a) ≤ lv b) ∨ (ord a d< ord b)
    lemma1 (case1 x) = ¬a x
-   lemma1 (case2 x) with d<→lv x
-   lemma1 (case2 x) | refl = ¬b refl
+   lemma1 (case2 x) = ⊥-elim (nat-≡< (sym ( d<→lv x )) c  )
 trio< a b | tri≈ ¬a refl ¬c with triOrdd ( ord a ) ( ord b )
 trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = tri< (case2 a) (λ refl → ¬b (lemma1 refl )) lemma2 where
    lemma1 :  (record { lv = _ ; ord = x }) ≡ b →  x ≡ ord b
@@ -273,13 +203,7 @@
 OrdTrans (case1 refl) (case1 refl) = case1 refl
 OrdTrans (case1 refl) (case2 lt2) = case2 lt2
 OrdTrans (case2 lt1) (case1 refl) = case2 lt1
-OrdTrans (case2 (case1 x)) (case2 (case1 y)) = case2 (case1 ( <-trans x y ) )
-OrdTrans (case2 (case1 x)) (case2 (case2 y)) with d<→lv y
-OrdTrans (case2 (case1 x)) (case2 (case2 y)) | refl = case2 (case1 x )
-OrdTrans (case2 (case2 x)) (case2 (case1 y)) with d<→lv x
-OrdTrans (case2 (case2 x)) (case2 (case1 y)) | refl = case2 (case1 y)
-OrdTrans (case2 (case2 x)) (case2 (case2 y)) with d<→lv x | d<→lv y
-OrdTrans (case2 (case2 x)) (case2 (case2 y)) | refl | refl = case2 (case2 (orddtrans x y ))
+OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y)
 
 OrdPreorder : {n : Level} → Preorder (suc n) (suc n) (suc n)
 OrdPreorder {n} = record { Carrier = Ordinal
@@ -293,12 +217,9 @@
  }
 
 TransFinite : {n : Level} → { ψ : Ordinal {n} → Set n }
-  → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } )) 
   → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
   → ( ∀ (lx : Nat ) → (x : OrdinalD lx )  → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
   →  ∀ (x : Ordinal)  → ψ x
-TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv } = caseΦ lv
-TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ } = caseOSuc lv ord₁
-    ( TransFinite caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
-TransFinite caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁
-
+TransFinite caseΦ caseOSuc record { lv = lv ; ord = (Φ (lv)) } = caseΦ lv
+TransFinite caseΦ caseOSuc record { lv = lx ; ord = (OSuc lx ox) } = 
+      caseOSuc lx ox (TransFinite caseΦ caseOSuc  record { lv = lx ; ord = ox })