I understand the need for a universe hierarchy, and that each new level brings additionnal proof-theoretic strength.

In the HoTT book there are examples of proofs that need to use the next level in the Universe hierarchy.

Do we have examples of inhabited types A:U(n), where the construction of the inhabitants/proof a:A requires the use of U(n+2) ?

  • $\begingroup$ Presumably, you could formulate a syntactic theory of HoTT restricted to some fixed number of universes inside of (full) HoTT. The consistency proof should then require at least that number of actual universes. $\endgroup$ May 27, 2018 at 18:34
  • $\begingroup$ I'm no expert on these matters, but I'm of the impression that higher universes can also be used to define faster-growing functions from the naturals to the naturals. So you could define $A$ to be the type of all functions having so-and-so growth behaviour, and then give an inhabitant of $A$ by employing higher universes. I can't say how to formalize this properly. $\endgroup$ May 30, 2018 at 19:58

1 Answer 1


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.