--- a/OD.agda	Wed Jul 15 08:42:30 2020 +0900
+++ b/OD.agda	Fri Jul 17 16:33:30 2020 +0900
@@ -146,7 +146,7 @@
 _c<_ : ( x a : HOD  ) → Set n
 x c< a = a ∋ x 
 
-cseq : {n : Level} →  HOD  →  HOD 
+cseq :  HOD  →  HOD 
 cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
     lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x)
     lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc ) 
@@ -154,7 +154,7 @@
 odef-subst :  {Z : HOD } {X : Ordinal  }{z : HOD } {x : Ordinal  }→ odef Z X → Z ≡ z  →  X ≡ x  →  odef z x
 odef-subst df refl refl = df
 
-otrans : {n : Level} {a x y : Ordinal  } → odef (Ord a) x → odef (Ord x) y → odef (Ord a) y
+otrans : {a x y : Ordinal  } → odef (Ord a) x → odef (Ord x) y → odef (Ord a) y
 otrans x<a y<x = ordtrans y<x x<a
 
 odef→o< :  {X : HOD } → {x : Ordinal } → odef X x → x o< od→ord X 
@@ -243,6 +243,10 @@
    lemma (case1 refl) = y∋x
    lemma (case2 refl) = y∋x
 
+-- another possible restriction. We reqest no minimality on odmax, so it may arbitrary larger.
+odmax<od→ord  : { x y : HOD } → x ∋ y →  Set n
+odmax<od→ord {x} {y} x∋y = odmax x o< od→ord x
+
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)