--- a/HOD.agda	Wed Jul 17 10:52:31 2019 +0900
+++ b/HOD.agda	Thu Jul 18 16:06:41 2019 +0900
@@ -72,6 +72,7 @@
   -- sup-x  : {n : Level } → ( Ordinal {n} → Ordinal {n}) →  Ordinal {n}
   -- sup-lb : {n : Level } → { ψ : Ordinal {n} →  Ordinal {n}} → {z : Ordinal {n}}  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
   -- sup-lb : {n : Level } → ( ψ : Ordinal {n} →  Ordinal {n}) → ( ∀ {x : Ordinal {n}} →  ψx  o<  z ) →  z o< osuc ( sup-o ψ ) 
+  -- mimimul and x∋minimul is a weaker form of Axiom of choice
   minimul : {n : Level } → (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 
   -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
   x∋minimul : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) )
@@ -202,6 +203,11 @@
 is-o∅ {n} record { lv = Zero ; ord = (OSuc .0 ord₁) } = no ( λ () )
 is-o∅ {n} record { lv = (Suc lv₁) ; ord = ord } = no (λ())
 
+OrdP : {n : Level} →  ( x : Ordinal {suc n} ) ( y : OD {suc n} ) → Dec ( Ord x ∋ y )
+OrdP {n} x y with trio< x (od→ord y)
+OrdP {n} x y | tri< a ¬b ¬c = no ¬c
+OrdP {n} x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
+OrdP {n} x y | tri> ¬a ¬b c = yes c
 
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
@@ -228,7 +234,7 @@
 L {n}  record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
     cseq ( Ord (od→ord (L {n}  (record { lv = lx ; ord = Φ lx }))))
 
--- L0 :  {n : Level} → (α : Ordinal {suc n}) → α o< β → L (osuc α) ∋ L α
+-- L0 :  {n : Level} → (α : Ordinal {suc n}) → L (osuc α) ∋ L α
 -- L1 :  {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : OD {suc n})  → L α ∋ x → L β ∋ x 
 
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
@@ -299,7 +305,7 @@
          proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B)
          proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B)
 
-         empty : (x : OD {suc n} ) → ¬  (od∅ ∋ x)
+         empty : {n : Level } (x : OD {suc n} ) → ¬  (od∅ ∋ x)
          empty x (case1 ())
          empty x (case2 ())
 
@@ -461,3 +467,16 @@
          choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A 
          choice X {A} X∋A not = x∋minimul A not
 
+         ε-induction : {n m : Level} { ψ : OD {suc n} → Set m}
+              → ( {x : OD {suc n} } → ({ y : OD {suc n} } →  x ∋ y → ψ y ) → ψ x )
+              → (x : OD {suc n} ) → ψ x
+         ε-induction {n} {m} {ψ} ind x with od→ord x  | oiso {suc n} {x}
+         ε-induction {n} {m} {ψ} ind x | record { lv = Zero ; ord = Φ 0 } | refl = ind (lemma o∅≡od∅  ) where
+               lemma : { y : OD {suc n} } → x ≡ od∅  → x ∋ y → ψ y 
+               lemma {y} eq lt with empty y (o<-subst (c<→o< lt) refl diso )
+               lemma {y} eq lt | ()
+         ε-induction {n} {m} {ψ} ind x | record { lv = Zero ; ord = OSuc 0 ox } | refl = {!!}
+         ε-induction {n} {m} {ψ} ind x | record { lv = Suc lx ; ord = Φ (Suc lx) } | refl = {!!}
+         ε-induction {n} {m} {ψ} ind x | record { lv = Suc lx ; ord = OSuc (Suc lx) ox } | refl = {!!}
+
+--              subst (λ k → ψ k ) oiso (TransFinite {suc n} {suc (suc n) ⊔ m} {λ x → ({y : Ordinal } → y o< x → ψ y ) → ψ (ord→od x) } {!!} {!!} {!!} {!!})

--- a/ordinal.agda	Wed Jul 17 10:52:31 2019 +0900
+++ b/ordinal.agda	Thu Jul 18 16:06:41 2019 +0900
@@ -313,7 +313,7 @@
      }
  }
 
-TransFinite : {n : Level} → { ψ : Ordinal {n} → Set n }
+TransFinite : {n m : Level} → { ψ : Ordinal {n} → Set m }
   → ( ∀ (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