# Zulip Chat Archive

## 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