universe enlargement

Stream: general

[Reid Barton]

Suppose I have a universe-polymorphic proposition P.{u} : Prop and a proof of P.{u0} as a term (either in the empty context, or, ideally, in a context which only contains variables whose types are Type v for v <= u0). Is it then true that I can also prove P.{u1}, for any u1 >= u0?

[Reid Barton]

Is this something I could prove just by inducting over the proof term?

[Reid Barton]

Obviously it depends on my axioms, since for example I could consistently assume that Type 0 has no inaccessibles, which I can prove is false in Type 1. I mean using the usual axioms of Lean.

[Mario Carneiro]

Let P.{u} = |Type u| < |Type 1| and u0 = 0

[Mario Carneiro]

You need only the usual axioms to prove that P.{0} is true and P.{1} is false

[Reid Barton]

Hmm, right. I need to find a better way to express what I mean.

[Mario Carneiro]

One true thing is that there is a model of lean where the universes are any increasing countable sequence of inaccessibles, not necessarily the minimal one, which suggests that it is possible to convert any proof using universes Type 0, ..., Type k into one using Type u_0, ..., Type u_k where u_0 < ... < u_k. However this is not so easy because of the existence of the universe successor function: Type 0 has type Type 1 but Type u_0 does not have type Type u_1. So this doesn't work without modification