Structural recursion for reflexive inductive type

Stream: lean4

[Parth Shastri]

In the following example, the definition of fold gives the error message invalid universe level, u is not greater than 0. However, changing the type of α to either Prop or Type u works. Is there any way to get a compiled definition that works for all universe levels?

inductive Ordinal
  | zero : Ordinal
  | succ : Ordinal → Ordinal
  | limit : (Nat → Ordinal) → Ordinal

variable {α : Sort u} (zero : α) (succ : α → α) (limit : (Nat → α) → α) in
def Ordinal.fold : Ordinal → α
  | .zero => zero
  | .succ o => succ (fold o)
  | .limit f => limit λ n => fold (f n)