# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1565407885 -32400
# Node ID afc864169325d540b3b9ac4168ae19e2d074691f
# Parent  2e1f19c949dcc78d4b789973f0e2b300576ecec0
recover ε-induction

diff -r 2e1f19c949dc -r afc864169325 cardinal.agda
--- a/cardinal.agda	Fri Aug 09 17:57:58 2019 +0900
+++ b/cardinal.agda	Sat Aug 10 12:31:25 2019 +0900
@@ -1,21 +1,22 @@
 open import Level
-module cardinal where
+open import Ordinals
+module cardinal {n : Level } (O : Ordinals {n}) where
 
 open import zf
-open import ordinal
 open import logic
-open import OD
+import OD 
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
-open import  Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality
 open import Data.Nat.Properties 
 open import Data.Empty
 open import Relation.Nullary
 open import Relation.Binary
 open import Relation.Binary.Core
 
+open inOrdinal O
+open OD O
 open OD.OD
 
-open Ordinal
 open _∧_
 open _∨_
 open Bool
@@ -27,30 +28,30 @@
 --     X ---------------------------> Y
 --          ymap   <-  def Y y
 --
-record Onto {n : Level } (X Y : OD {n})  : Set (suc n) where
+record Onto  (X Y : OD )  : Set n where
    field
-       xmap : (x : Ordinal {n}) → def X x → Ordinal {n} 
-       ymap : (y : Ordinal {n}) → def Y y → Ordinal {n} 
-       ymap-on-X  : {y :  Ordinal {n} } → (lty : def Y y ) → def X (ymap y lty)  
-       onto-iso   : {y :  Ordinal {n} } → (lty : def Y y ) → xmap  ( ymap y lty ) (ymap-on-X lty ) ≡ y
+       xmap : (x : Ordinal ) → def X x → Ordinal  
+       ymap : (y : Ordinal ) → def Y y → Ordinal  
+       ymap-on-X  : {y :  Ordinal  } → (lty : def Y y ) → def X (ymap y lty)  
+       onto-iso   : {y :  Ordinal  } → (lty : def Y y ) → xmap  ( ymap y lty ) (ymap-on-X lty ) ≡ y
 
-record Cardinal {n : Level } (X  : OD {n}) : Set (suc n) where
+record Cardinal  (X  : OD ) : Set n where
    field
-       cardinal : Ordinal {n}
+       cardinal : Ordinal 
        conto : Onto (Ord cardinal) X 
-       cmax : ( y : Ordinal {n} ) → cardinal o< y → ¬ Onto (Ord y) X 
+       cmax : ( y : Ordinal  ) → cardinal o< y → ¬ Onto (Ord y) X 
 
-cardinal : {n : Level } (X  : OD {suc n}) → Cardinal X
-cardinal {n} X = record {
+cardinal :  (X  : OD ) → Cardinal X
+cardinal  X = record {
        cardinal = sup-o ( λ x → proj1 ( cardinal-p x) )
      ; conto = onto
      ; cmax = cmax
    } where
-    cardinal-p : (x  : Ordinal {suc n}) →  ( Ordinal {suc n} ∧ Dec (Onto (Ord x) X) )
+    cardinal-p : (x  : Ordinal ) →  ( Ordinal  ∧ Dec (Onto (Ord x) X) )
     cardinal-p x with p∨¬p ( Onto (Ord x) X ) 
     cardinal-p x | case1 True = record { proj1 = x ; proj2 = yes True }
     cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False }
-    onto-set : OD {suc n}
+    onto-set : OD 
     onto-set = record { def = λ x →  {!!} } -- Onto (Ord (sup-o (λ x → proj1 (cardinal-p x)))) X }
     onto : Onto (Ord (sup-o (λ x → proj1 (cardinal-p x)))) X
     onto = record {
@@ -63,37 +64,37 @@
        -- Ord cardinal itself has no onto map, but if we have x o< cardinal, there is one
        --    od→ord X o< cardinal, so if we have def Y y or def X y, there is an Onto (Ord y) X
        Y = (Ord (sup-o (λ x → proj1 (cardinal-p x))))
-       lemma1 : (y : Ordinal {suc n}) → def Y y  →  Onto (Ord y) X
-       lemma1 y y<Y with sup-o< {suc n} {λ x → proj1 ( cardinal-p x)} {y} 
+       lemma1 : (y : Ordinal ) → def Y y  →  Onto (Ord y) X
+       lemma1 y y<Y with sup-o<  {λ x → proj1 ( cardinal-p x)} {y} 
        ... | t = {!!}
        lemma2 :  def Y (od→ord X)
        lemma2 = {!!}
-       xmap : (x : Ordinal {suc n}) → def Y x → Ordinal {suc n}
+       xmap : (x : Ordinal ) → def Y x → Ordinal 
        xmap = {!!}
-       ymap : (y : Ordinal {suc n}) → def X y → Ordinal {suc n}
+       ymap : (y : Ordinal ) → def X y → Ordinal 
        ymap = {!!}
-       ymap-on-X  : {y :  Ordinal {suc n} } → (lty : def X y ) → def Y (ymap y lty)  
+       ymap-on-X  : {y :  Ordinal  } → (lty : def X y ) → def Y (ymap y lty)  
        ymap-on-X  = {!!}
-       onto-iso   : {y :  Ordinal {suc n} } → (lty : def X y ) → xmap  (ymap y lty) (ymap-on-X lty ) ≡ y
+       onto-iso   : {y :  Ordinal  } → (lty : def X y ) → xmap  (ymap y lty) (ymap-on-X lty ) ≡ y
        onto-iso = {!!}
     cmax : (y : Ordinal) → sup-o (λ x → proj1 (cardinal-p x)) o< y → ¬ Onto (Ord y) X
-    cmax y lt ontoy = o<> lt (o<-subst {suc n} {_} {_} {y} {sup-o (λ x → proj1 (cardinal-p x))}
-       (sup-o< {suc n} {λ x → proj1 ( cardinal-p x)}{y}  ) lemma refl ) where
+    cmax y lt ontoy = o<> lt (o<-subst  {_} {_} {y} {sup-o (λ x → proj1 (cardinal-p x))}
+       (sup-o<  {λ x → proj1 ( cardinal-p x)}{y}  ) lemma refl ) where
           lemma : proj1 (cardinal-p y) ≡ y
           lemma with  p∨¬p ( Onto (Ord y) X )
           lemma | case1 x = refl
           lemma | case2 not = ⊥-elim ( not ontoy )
 
-func : {n : Level}  → (f : Ordinal {suc n} → Ordinal {suc n}) → OD {suc n}
-func {n} f = record { def = λ y → (x : Ordinal {suc n}) → y ≡ f x }
+func : (f : Ordinal  → Ordinal ) → OD 
+func  f = record { def = λ y → (x : Ordinal ) → y ≡ f x }
 
-Func : {n : Level}  → OD {suc n}
-Func {n} = record { def = λ x →  (f : Ordinal {suc n} → Ordinal {suc n}) → x ≡ od→ord (func f) }
+Func : OD 
+Func  = record { def = λ x →  (f : Ordinal  → Ordinal ) → x ≡ od→ord (func f) }
 
-odmap : {n : Level}  → { x : OD {suc n} } → Func ∋ x → Ordinal {suc n} → OD {suc n}
-odmap {n} {f} lt x = record { def = λ y → def f y } 
+odmap : { x : OD  } → Func ∋ x → Ordinal  → OD 
+odmap  {f} lt x = record { def = λ y → def f y } 
 
-lemma1 :  {n : Level}  → { x : OD {suc n} } → Func ∋ x → {!!} -- ¬ ( (f : Ordinal {suc n} → Ordinal {suc n}) →  ¬ ( x ≡ od→ord (func f)  ))
+lemma1 :  { x : OD  } → Func ∋ x → {!!} -- ¬ ( (f : Ordinal  → Ordinal ) →  ¬ ( x ≡ od→ord (func f)  ))
 lemma1 = {!!}
 
 
diff -r 2e1f19c949dc -r afc864169325 ordinal.agda
--- a/ordinal.agda	Fri Aug 09 17:57:58 2019 +0900
+++ b/ordinal.agda	Sat Aug 10 12:31:25 2019 +0900
@@ -29,12 +29,6 @@
 _o<_ : {n : Level} ( x y : Ordinal ) → Set n
 _o<_ x y =  (lv x < lv y )  ∨ ( ord x d< ord y )
 
-o<-dom :  {n : Level} { x y : Ordinal {n}} → x o< y → Ordinal 
-o<-dom {n} {x} _ = x
-
-o<-cod :  {n : Level} { x y : Ordinal {n}} → x o< y → Ordinal 
-o<-cod {n} {_} {y} _ = y
-
 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 
@@ -66,12 +60,6 @@
       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
 
@@ -81,9 +69,6 @@
 trio>≡ : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → y d< x → ⊥
 trio>≡ refl = ≡→¬d<
 
-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
-
 triOrdd : {n : Level} →  {lx : Nat}   → Trichotomous  _≡_ ( _d<_  {n} {lx} {lx} )
 triOrdd  {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d<
 triOrdd  {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< )
@@ -100,22 +85,6 @@
 <-osuc {n} {record { lv = lx ; ord = Φ .lx }} =  case2 Φ<
 <-osuc {n} {record { lv = lx ; ord = OSuc .lx ox }} = case2 ( s< s<refl )
 
-osuc-lveq : {n : Level} { x : Ordinal {n} } → lv x ≡ lv ( osuc x )
-osuc-lveq {n} = refl
-
-osucc : {n : Level} {ox oy : Ordinal {n}} → oy o< ox  → osuc oy o< osuc ox
-osucc {n} {ox} {oy} (case1 x) = case1 x
-osucc {n} {ox} {oy} (case2 x) with d<→lv x
-... | refl = case2 (s< x)
-
-case12-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord x d< ord y → ⊥
-case12-⊥ {x} {y} lt1 lt2 with d<→lv lt2
-... | refl = nat-≡< refl lt1
-
-case21-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord y d< ord x → ⊥
-case21-⊥ {x} {y} lt1 lt2 with d<→lv lt2
-... | refl = nat-≡< refl lt1
-
 o<¬≡ : {n : Level } { ox oy : Ordinal {suc n}} → ox ≡ oy  → ox o< oy  → ⊥
 o<¬≡ {_} {ox} {ox} refl (case1 lt) =  =→¬< lt
 o<¬≡ {_} {ox} {ox} refl (case2 (s< lt)) = trio<≡ refl lt
@@ -156,20 +125,6 @@
 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αd : {n : Level} → { lx : Nat } → OrdinalD {n} lx  →  OrdinalD  lx  →  OrdinalD  lx
-maxαd x y with triOrdd x y
-maxαd x y | tri< a ¬b ¬c = y
-maxαd x y | tri≈ ¬a b ¬c = x
-maxαd x y | tri> ¬a ¬b c = x
-
-minαd : {n : Level} → { lx : Nat } → OrdinalD {n} lx  →  OrdinalD  lx  →  OrdinalD  lx
-minαd x y with triOrdd x y
-minαd x y | tri< a ¬b ¬c = x
-minαd x y | tri≈ ¬a b ¬c = y
-minαd x y | tri> ¬a ¬b c = x
-
-_o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n)
-a o≤ b  = (a ≡ b)  ∨ ( a o< b )
 
 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₂ )
@@ -208,99 +163,9 @@
    lemma1 (case1 x) = ¬a x
    lemma1 (case2 x) = ≡→¬d< x
 
-xo<ab : {n : Level} {oa ob : Ordinal {suc n}} → ( {ox : Ordinal {suc n}} → ox o< oa  → ox o< ob ) → oa o< osuc ob
-xo<ab {n}  {oa} {ob} a→b with trio< oa ob
-xo<ab {n}  {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc
-xo<ab {n}  {oa} {ob} a→b | tri≈ ¬a refl ¬c = <-osuc
-xo<ab {n}  {oa} {ob} a→b | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c )  )
-
-maxα : {n : Level} →  Ordinal {suc n} →  Ordinal  → Ordinal
-maxα x y with trio< x y
-maxα x y | tri< a ¬b ¬c = y
-maxα x y | tri> ¬a ¬b c = x
-maxα x y | tri≈ ¬a refl ¬c = x
-
-minα : {n : Level} →  Ordinal {suc n} →  Ordinal  → Ordinal
-minα {n} x y with trio< {n} x  y
-minα x y | tri< a ¬b ¬c = x
-minα x y | tri> ¬a ¬b c = y
-minα x y | tri≈ ¬a refl ¬c = x
-
-min1 : {n : Level} →  {x y z : Ordinal {suc n} } → z o< x → z o< y → z o< minα x y
-min1 {n} {x} {y} {z} z<x z<y with trio< {n} x y
-min1 {n} {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x
-min1 {n} {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x
-min1 {n} {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y
-
---
---  max ( osuc x , osuc y )
---
-
-omax : {n : Level} ( x y : Ordinal {suc n} ) → Ordinal {suc n}
-omax {n} x y with trio< x y
-omax {n} x y | tri< a ¬b ¬c = osuc y
-omax {n} x y | tri> ¬a ¬b c = osuc x
-omax {n} x y | tri≈ ¬a refl ¬c  = osuc x
-
-omax< : {n : Level} ( x y : Ordinal {suc n} ) → x o< y → osuc y ≡ omax x y
-omax< {n} x y lt with trio< x y
-omax< {n} x y lt | tri< a ¬b ¬c = refl
-omax< {n} x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt )
-omax< {n} x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt )
-
-omax≡ : {n : Level} ( x y : Ordinal {suc n} ) → x ≡ y → osuc y ≡ omax x y
-omax≡ {n} x y eq with trio< x y
-omax≡ {n} x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq )
-omax≡ {n} x y eq | tri≈ ¬a refl ¬c = refl
-omax≡ {n} x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq )
-
-omax-x : {n : Level} ( x y : Ordinal {suc n} ) → x o< omax x y
-omax-x {n} x y with trio< x y
-omax-x {n} x y | tri< a ¬b ¬c = ordtrans a <-osuc
-omax-x {n} x y | tri> ¬a ¬b c = <-osuc
-omax-x {n} x y | tri≈ ¬a refl ¬c = <-osuc
-
-omax-y : {n : Level} ( x y : Ordinal {suc n} ) → y o< omax x y
-omax-y {n} x y with  trio< x y
-omax-y {n} x y | tri< a ¬b ¬c = <-osuc
-omax-y {n} x y | tri> ¬a ¬b c = ordtrans c <-osuc
-omax-y {n} x y | tri≈ ¬a refl ¬c = <-osuc
-
-omxx : {n : Level} ( x : Ordinal {suc n} ) → omax x x ≡ osuc x
-omxx {n} x with  trio< x x
-omxx {n} x | tri< a ¬b ¬c = ⊥-elim (¬b refl )
-omxx {n} x | tri> ¬a ¬b c = ⊥-elim (¬b refl )
-omxx {n} x | tri≈ ¬a refl ¬c = refl
-
-omxxx : {n : Level} ( x : Ordinal {suc n} ) → omax x (omax x x ) ≡ osuc (osuc x)
-omxxx {n} x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc ))
 
 open _∧_
 
-osuc2 : {n : Level} ( x y : Ordinal {suc n} ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
-proj1 (osuc2 {n} x y) (case1 lt) = case1 lt
-proj1 (osuc2 {n} x y) (case2 (s< lt)) = case2 lt
-proj2 (osuc2 {n} x y) (case1 lt) = case1 lt
-proj2 (osuc2 {n} x y) (case2 lt) with d<→lv lt
-... | refl = case2 (s< lt)
-
-OrdTrans : {n : Level} → Transitive {suc n} _o≤_
-OrdTrans (case1 refl) (case1 refl) = case1 refl
-OrdTrans (case1 refl) (case2 lt2) = case2 lt2
-OrdTrans (case2 lt1) (case1 refl) = case2 lt1
-OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y)
-
-OrdPreorder : {n : Level} → Preorder (suc n) (suc n) (suc n)
-OrdPreorder {n} = record { Carrier = Ordinal
-   ; _≈_  = _≡_ 
-   ; _∼_   = _o≤_
-   ; isPreorder   = record {
-        isEquivalence = record { refl = refl  ; sym = sym ; trans = trans }
-        ; reflexive     = case1 
-        ; trans         = OrdTrans 
-     }
- }
-
 TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m }
   → ( ∀ (lx : Nat ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx)  → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
   → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ( (y : Ordinal {suc n} ) → y o< ordinal lx (OSuc lx x)  → ψ y )   → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
@@ -355,9 +220,9 @@
   → ¬ p
 TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 
 
-open import Ordinals
+open import Ordinals 
 
-C-Ordinal : {n : Level } → Ordinals {suc n} 
+C-Ordinal : {n : Level} →  Ordinals {suc n} 
 C-Ordinal {n} = record {
      ord = Ordinal {suc n}
    ; o∅ = o∅
@@ -384,3 +249,142 @@
         caseOSuc :  (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
             ψ (record { lv = lx ; ord = OSuc lx x₁ })
         caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev 
+
+module C-Ordinal-with-choice {n : Level} where
+
+  import OD 
+  -- open inOrdinal C-Ordinal 
+  open OD (C-Ordinal {n})
+  open OD.OD
+  
+  --
+  -- another form of regularity 
+  --
+  ε-induction : {m : Level} { ψ : OD  → Set m}
+   → ( {x : OD } → ({ y : OD } →  x ∋ y → ψ y ) → ψ x )
+   → (x : OD ) → ψ x
+  ε-induction {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (lv (osuc (od→ord x))) (ord (osuc (od→ord x)))  <-osuc) where
+    ε-induction-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly }
+      → (ly < lx) ∨ (oy d< ox  ) → ψ (ord→od (record { lv = ly ; ord = oy } ) )
+    ε-induction-ord lx  (OSuc lx ox) {ly} {oy} y<x = 
+      ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord lx ox (lemma y lt ))) where
+          lemma :  (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → od→ord z o< record { lv = lx ; ord = ox }
+          lemma z lt with osuc-≡< y<x
+          lemma z lt | case1 refl = o<-subst (c<→o< lt) refl diso
+          lemma z lt | case2 lt1 = ordtrans  (o<-subst (c<→o< lt) refl diso) lt1  
+    ε-induction-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} (case1 y<sox ) =                    
+      ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → lemma y lt )  where  
+          --
+          --     if lv of z if less than x Ok
+          --     else lv z = lv x. We can create OSuc of z which is larger than z and less than x in lemma
+          --
+          --                         lx    Suc lx      (1) lz(a) <lx by case1
+          --                 ly(1)   ly(2)             (2) lz(b) <lx by case1
+          --           lz(a) lz(b)   lz(c)                 lz(c) <lx by case2 ( ly==lz==lx)
+          --
+          lemma0 : { lx ly : Nat } → ly < Suc lx  → lx < ly → ⊥
+          lemma0 {Suc lx} {Suc ly} (s≤s lt1) (s≤s lt2) = lemma0 lt1 lt2
+          lemma1 : {ly : Nat} {oy : OrdinalD {suc n} ly} → lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) ≡ ly
+          lemma1  {ly} {oy} = let open ≡-Reasoning in begin
+                  lv (od→ord (ord→od (record { lv = ly ; ord = oy })))
+               ≡⟨ cong ( λ k → lv k ) diso ⟩
+                  lv (record { lv = ly ; ord = oy })
+               ≡⟨⟩
+                  ly
+               ∎
+          lemma :  (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → ψ z
+          lemma z lt with  c<→o<  {z} {ord→od (record { lv = ly ; ord = oy })} lt
+          lemma z lt | case1 lz<ly with <-cmp lx ly
+          lemma z lt | case1 lz<ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen
+          lemma z lt | case1 lz<ly | tri≈ ¬a refl ¬c =    -- ly(1)
+                subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → lv (od→ord z) < k ) lemma1 lz<ly ) ))
+          lemma z lt | case1 lz<ly | tri> ¬a ¬b c =       -- lz(a)
+                subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (<-trans lz<ly (subst (λ k → k < lx ) (sym lemma1) c))))
+          lemma z lt | case2 lz=ly with <-cmp lx ly
+          lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen
+          lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly        -- lz(b)
+          ... | eq = subst (λ k → ψ k ) oiso
+               (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c )))
+          lemma z lt | case2 lz=ly | tri≈ ¬a lx=ly ¬c with d<→lv lz=ly    -- lz(c)
+          ... | eq =  subst (λ k → ψ k ) oiso ( ε-induction-ord lx (dz oz=lx) {lv (od→ord z)} {ord (od→ord z)} (case2 (dz<dz oz=lx) )) where
+              oz=lx : lv (od→ord z) ≡ lx 
+              oz=lx = let open ≡-Reasoning in begin
+                  lv (od→ord z)
+                 ≡⟨ eq ⟩
+                  lv (od→ord (ord→od (ordinal ly oy)))
+                 ≡⟨ cong ( λ k → lv k ) diso ⟩
+                  lv (ordinal ly oy)
+                 ≡⟨ sym lx=ly  ⟩
+                  lx
+                 ∎
+              dz : lv (od→ord z) ≡ lx → OrdinalD lx
+              dz refl = OSuc lx (ord (od→ord z))
+              dz<dz  : (z=x : lv (od→ord z) ≡ lx ) → ord (od→ord z) d< dz z=x
+              dz<dz refl = s<refl 
+  
+  ---
+  --- With assuption of OD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
+  ---
+  record choiced  ( X : OD) : Set (suc (suc n)) where
+   field
+      a-choice : OD
+      is-in : X ∋ a-choice
+  
+  choice-func' :  (X : OD ) → (p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X
+  choice-func'  X p∨¬p not = have_to_find where
+          ψ : ( ox : Ordinal {suc n}) → Set (suc (suc n))
+          ψ ox = (( x : Ordinal {suc n}) → x o< ox  → ( ¬ def X x )) ∨ choiced X
+          lemma-ord : ( ox : Ordinal {suc n} ) → ψ ox
+          lemma-ord  ox = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc1 ox where
+             ∋-p' : (A x : OD ) → Dec ( A ∋ x ) 
+             ∋-p' A x with p∨¬p ( A ∋ x )
+             ∋-p' A x | case1 t = yes t
+             ∋-p' A x | case2 t = no t
+             ∀-imply-or :  {n : Level}  {A : Ordinal {suc n} → Set (suc n) } {B : Set (suc (suc n)) }
+                 → ((x : Ordinal {suc n}) → A x ∨ B) →  ((x : Ordinal {suc n}) → A x) ∨ B
+             ∀-imply-or {n} {A} {B} ∀AB with p∨¬p  ((x : Ordinal {suc n}) → A x)
+             ∀-imply-or {n} {A} {B} ∀AB | case1 t = case1 t
+             ∀-imply-or {n} {A} {B} ∀AB | case2 x = case2 (lemma x) where
+                  lemma : ¬ ((x : Ordinal {suc n}) → A x) →  B
+                  lemma not with p∨¬p B
+                  lemma not | case1 b = b
+                  lemma not | case2 ¬b = ⊥-elim  (not (λ x → dont-orb (∀AB x) ¬b ))
+             caseΦ : (lx : Nat) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x) → ψ (ordinal lx (Φ lx) ) 
+             caseΦ lx prev with ∋-p' X ( ord→od (ordinal lx (Φ lx) ))
+             caseΦ lx prev | yes p = case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } )
+             caseΦ lx prev | no ¬p = lemma where
+                  lemma1 : (x : Ordinal) → (((Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X)
+                  lemma1 x with trio< x (ordinal lx (Φ lx))
+                  lemma1 x | tri< a ¬b ¬c with prev (osuc x) (lemma2 a) where
+                      lemma2 : x o< (ordinal lx (Φ lx)) →  osuc x o< ordinal lx (Φ lx)
+                      lemma2 (case1 lt) = case1 lt
+                  lemma1 x | tri< a ¬b ¬c | case2 found = case2 found
+                  lemma1 x | tri< a ¬b ¬c | case1 not_found = case1 ( λ lt df → not_found x <-osuc df )
+                  lemma1 x | tri≈ ¬a refl ¬c = case1 ( λ lt → ⊥-elim (o<¬≡ refl lt ))
+                  lemma1 x | tri> ¬a ¬b c = case1 ( λ lt → ⊥-elim (o<> lt c ))
+                  lemma : ((x : Ordinal) → (Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X
+                  lemma = ∀-imply-or lemma1
+             caseOSuc : (lx : Nat) (x : OrdinalD lx) → ψ ( ordinal lx x ) → ψ ( ordinal lx (OSuc lx x) )
+             caseOSuc lx x prev with ∋-p' X (ord→od record { lv = lx ; ord = x } )
+             caseOSuc lx x prev | yes p = case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p })
+             caseOSuc lx x (case1 not_found) | no ¬p = case1 lemma where
+                  lemma : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx x) → def X y → ⊥
+                  lemma y lt with trio< y (ordinal lx x )
+                  lemma y lt | tri< a ¬b ¬c = not_found y a
+                  lemma y lt | tri≈ ¬a refl ¬c = subst (λ k → def X k → ⊥ ) diso ¬p
+                  lemma y lt | tri> ¬a ¬b c with osuc-≡< lt
+                  lemma y lt | tri> ¬a ¬b c | case1 refl = ⊥-elim ( ¬b refl )
+                  lemma y lt | tri> ¬a ¬b c | case2 lt1 = ⊥-elim (o<> c lt1 )
+             caseOSuc lx x (case2 found) | no ¬p = case2 found
+             caseOSuc1 : (lx : Nat) (x : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x) → ψ y) →
+                 ψ (record { lv = lx ; ord = OSuc lx x })
+             caseOSuc1 lx x lt =  caseOSuc lx x (lt ( ordinal lx x ) (case2 s<refl))
+          have_to_find : choiced X
+          have_to_find with lemma-ord (od→ord X )
+          have_to_find | t = dont-or  t ¬¬X∋x where
+              ¬¬X∋x : ¬ ((x : Ordinal) → (Suc (lv x) ≤ lv (od→ord X)) ∨ (ord x d< ord (od→ord X)) → def X x → ⊥)
+              ¬¬X∋x nn = not record {
+                     eq→ = λ {x} lt → ⊥-elim  (nn x (def→o< lt) lt) 
+                   ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
+                 }
+