This question on the theoretical CS stack exchange asks if pentation is implementable on Church numerals in a predicative variant of System F. In the normal, impredicative system, this is quite easy, because we have:
ℕ : Type
ℕ = forall (R : Type). (R -> R) -> (R -> R)
1 : ℕ
1 R s z = s z
hyper : (ℕ -> ℕ -> ℕ) -> (ℕ -> ℕ -> ℕ)
hyper op m n = n ℕ (op m) 1
So, because a Church numeral can be instantiated to work on the type of Church numerals, we can easily iterate an operation to get to the next hyper operation.
However, in a predicative system, the quantification over types increases the size of the quantifying type to be larger than the size of the types quantified over. So, a Church numeral that can be instantiated to operate on Church numerals must be one that quantifies over a higher universe.
The person asking the question links to a paper on the functions representable in such a stratified system with $\omega$ universe levels (I.E. one for each natural number). The paper shows that the representable functions are the super-elementary functions, which includes tetration, particular finite compositions of tetration, and products and sums of those functions. However, the only reason that all these functions are even representable is that they make use of Church numerals for all universes. So, for instance, tetration has a type (something) like:
_^^_ : Church 0 -> Church 1 -> Church 0
That is, to compute tetration for 0-level numerals, you must make use of higher level numerals. And depending on the complexity of the function, you may have to use much higher levels to compute 0-level numerals (arbitrarily high levels).
I showed in the answer there how if you add even more universes, it is possible to give a uniform type for tetration, which then means pentation can be defined. But now the universes involved are indexed by transfinite ordinals (if at all), and you still (seem to) need to go up levels to define some functions on lower (but still very high) levels.