equiv and universes

Stream: maths

[Kevin Buzzard]

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]

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]

the last one isn't a puzzle

[Kevin Buzzard]

it unfortunately doesn't typecheck because of universe issues

[Kevin Buzzard]

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

[Reid Barton]

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]

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]

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