--- a/Ordinals.agda	Fri Jul 03 21:39:10 2020 +0900
+++ b/Ordinals.agda	Fri Jul 03 21:58:01 2020 +0900
@@ -13,14 +13,15 @@
 open import Relation.Binary
 open import Relation.Binary.Core
 
-record IsOrdinals {n : Level} (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where
+record IsOrdinals {n : Level} (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
    field
      Otrans :  {x y z : ord }  → x o< y → y o< z → x o< z
      OTri : Trichotomous {n} _≡_  _o<_ 
      ¬x<0 :   { x  : ord  } → ¬ ( x o< o∅  )
      <-osuc :  { x : ord  } → x o< osuc x
      osuc-≡< :  { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)  
-     is-limit :  { x : ord  } → Dec ( ¬ ((y : ord) → x ≡ osuc y) )
+     is-limit :  ( x : ord  ) → Dec ( ¬ ((y : ord) → x ≡ osuc y) )
+     next-limit : { x : ord } → (x o< next x )∧ (¬ ((y : ord) → next x ≡ osuc y) )
      TransFinite : { ψ : ord  → Set (suc n) }
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
@@ -32,7 +33,8 @@
      o∅ : ord
      osuc : ord → ord
      _o<_ : ord → ord → Set n
-     isOrdinal : IsOrdinals ord o∅ osuc _o<_
+     next :  ord → ord
+     isOrdinal : IsOrdinals ord o∅ osuc _o<_ next
 
 module inOrdinal  {n : Level} (O : Ordinals {n} ) where
 
@@ -48,10 +50,14 @@
         o∅ :   Ordinal  
         o∅ = Ordinals.o∅ O
 
+        next :   Ordinal → Ordinal
+        next = Ordinals.next O
+
         ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O)
         osuc-≡< = IsOrdinals.osuc-≡<  (Ordinals.isOrdinal O)
         <-osuc = IsOrdinals.<-osuc  (Ordinals.isOrdinal O)
         TransFinite = IsOrdinals.TransFinite  (Ordinals.isOrdinal O)
+        next-limit = IsOrdinals.next-limit  (Ordinals.isOrdinal O)
         
         o<-dom :   { x y : Ordinal } → x o< y → Ordinal 
         o<-dom  {x} _ = x