--- a/ordinal.agda	Sat Jul 04 12:53:40 2020 +0900
+++ b/ordinal.agda	Sat Jul 04 18:18:17 2020 +0900
@@ -211,6 +211,7 @@
    ; o∅ = o∅
    ; osuc = osuc
    ; _o<_ = _o<_
+   ; next = ?
    ; isOrdinal = record {
        Otrans = ordtrans
      ; OTri = trio<
@@ -218,14 +219,16 @@
      ; <-osuc = <-osuc
      ; osuc-≡< = osuc-≡<
      ; TransFinite = TransFinite1
+     ; is-limit = ?
+     ; next-limit = ?
    }
   } where
      ord1 : Set (suc n)
      ord1 = Ordinal {suc n}
-     TransFinite1 : { ψ : ord1  → Set (suc (suc n)) }
+     TransFinite1 : { ψ : ord1  → Set (suc n) }
           → ( (x : ord1)  → ( (y : ord1  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord1)  → ψ x
-     TransFinite1 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where
+     TransFinite1 {ψ} lt x = TransFinite {n} {suc n} {ψ} caseΦ caseOSuc x where
         caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
             ψ (record { lv = lx ; ord = Φ lx })
         caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev