## Stream: general

### Topic: universe enlargement

#### Reid Barton (Apr 22 2020 at 13:12):

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 (Apr 22 2020 at 13:12):

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

#### Reid Barton (Apr 22 2020 at 13:12):

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 (Apr 22 2020 at 14:01):

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

#### Mario Carneiro (Apr 22 2020 at 14:03):

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

#### Reid Barton (Apr 22 2020 at 14:12):

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

#### Mario Carneiro (Apr 22 2020 at 14:17):

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

Last updated: May 06 2021 at 21:09 UTC