--- a/OD.agda	Sat Aug 01 18:05:23 2020 +0900
+++ b/OD.agda	Sat Aug 01 23:37:10 2020 +0900
@@ -13,9 +13,13 @@
 open import Relation.Binary.Core
 
 open import logic
+import OrdUtil
 open import nat
 
-open inOrdinal O
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal 
+open Ordinals.IsNext isNext 
+open OrdUtil O
 
 -- Ordinal Definable Set
 
@@ -258,12 +262,12 @@
     lemma : {z : Ordinal} → (z ≡ & x) ∨ (z ≡ & x) → & x ≡ z
     lemma (case1 refl) = refl
     lemma (case2 refl) = refl
-    y⊆x,x : {z : Ordinals.ord O} → def (od (x , x)) z → def (od y) z
+    y⊆x,x : {z : Ordinal} → def (od (x , x)) z → def (od y) z
     y⊆x,x {z} lt = subst (λ k → def (od y) k ) (lemma lt) y∋x 
     lemma1 : osuc (& y) o< & (x , x)
     lemma1 = subst (λ k → osuc (& y) o< k ) (sym (peq {x})) (osucc c ) 
 
-ε-induction : { ψ : HOD  → Set n}
+ε-induction : { ψ : HOD  → Set (suc n)}
    → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
    → (x : HOD ) → ψ x
 ε-induction {ψ} ind x = subst (λ k → ψ k ) *iso (ε-induction-ord (osuc (& x)) <-osuc )  where
@@ -272,16 +276,6 @@
      ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (* oy)
      ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (* oy)} induction oy
 
--- level trick (what'a shame) for LEM / minimal
-ε-induction1 : { ψ : HOD  → Set (suc n)}
-   → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
-   → (x : HOD ) → ψ x
-ε-induction1 {ψ} ind x = subst (λ k → ψ k ) *iso (ε-induction-ord (osuc (& x)) <-osuc )  where
-     induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (* oy)) → ψ (* ox)
-     induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) *iso (prev (& y) (o<-subst (c<→o< lt) refl &iso ))) 
-     ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (* oy)
-     ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (* oy)} induction oy
-
 Select : (X : HOD  ) → ((x : HOD  ) → Set n ) → HOD 
 Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( * x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
 
@@ -591,7 +585,7 @@
     ;   power→ = power→  
     ;   power← = power← 
     ;   extensionality = λ {A} {B} {w} → extensionality {A} {B} {w} 
-    ;   ε-induction = ε-induction 
+    ;   ε-induction = ε-induction
     ;   infinity∅ = infinity∅
     ;   infinity = infinity
     ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}