## Stream: maths

### Topic: equiv and universes

#### Kevin Buzzard (Apr 29 2018 at 00:56):

I am interested in beefing up equiv but I am only now coming to terms with how universes work and do not yet really understand how they affect the picture if at all

#### Kevin Buzzard (Apr 29 2018 at 00:57):

import data.equiv
universes u v y z
def αu (X Y : Type u) := X  Y
def αuv (X : Type u) (Y : Type v) := X  Y
def αv (X Y : Type v) := X  Y

definition u_v {X : Type z} {Y : Type z} : equiv (αu X Y) (αv X Y) :=
{ to_fun := λ f,f,
inv_fun := λ f,f,
left_inv := λ x,rfl,
right_inv := λ x,rfl,
}

definition u_uv {X : Type z} {Y : Type z} : equiv (αu X Y) (αuv X Y) :=
{ to_fun := λ f,f,
inv_fun := λ f,f,
left_inv := λ x,rfl,
right_inv := λ x,rfl,
}

definition u_uv {X : Type u} {Y : Type v} : equiv (αu X Y) (\auv X Y) := sorry

#### Kevin Buzzard (Apr 29 2018 at 00:57):

the last one isn't a puzzle

#### Kevin Buzzard (Apr 29 2018 at 00:57):

it unfortunately doesn't typecheck because of universe issues

#### Kevin Buzzard (Apr 29 2018 at 00:58):

Is there any way of somehow forcing it to typecheck with universe coercion or something? And then would equiv still fail?

#### Reid Barton (Apr 29 2018 at 01:49):

I guess the zeroth thing to know about universes is that universe u doesn't mean "Fix a universe $U$"; it just makes u a legal thing to put somewhere that a universe is expected.
In other words, the u and vs in \au, \auv, \av are unrelated, and definitions \au and \av are exactly the same.

#### Reid Barton (Apr 29 2018 at 01:55):

You can think of Lean universes as corresponding to Grothendieck universes except that Lean universes are not cumulative, so that a type belongs to Type u for just one u.

#### Reid Barton (Apr 29 2018 at 02:05):

To "move" a type from one universe to a bigger one, use ulift. The new type is equiv to the old one (equiv.ulift).

Last updated: May 06 2021 at 17:38 UTC