Zulip Chat Archive

Stream: maths

Topic: equiv and universes


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 00:57):

the last one isn't a puzzle

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 00:57):

it unfortunately doesn't typecheck because of universe issues

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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