Zulip Chat Archive

Stream: new members

Topic: Lift a type to a higher universe


view this post on Zulip Jannis Limperg (Mar 28 2020 at 19:51):

Hey! I'm looking for this type, which surely exists somewhere in the standard library:

universes u v

inductive Lift (α : Type u) : Type (max u v)
| Lift_intro : α  Lift

(library_search and suggest didn't bring up anything.)

view this post on Zulip Reid Barton (Mar 28 2020 at 19:56):

ulift

view this post on Zulip Jannis Limperg (Mar 28 2020 at 20:04):

Thanks!

view this post on Zulip Kevin Buzzard (Mar 28 2020 at 20:18):

I think it's worth just quoting Lean's definition here, because I think it's a rather beautiful part of the core library:

structure {r s} ulift (α : Type s) : Type (max s r) :=
up :: (down : α)

up and down and ulift are all defined simultaneously. It's not often you see the use of Lean's ability to name the constructor of a structure something other than mk.

ulift.up : Π {α : Type s}, α → ulift α
ulift.down : Π {α : Type s}, ulift α → α

I still remember where I was when I first spent several minutes staring at this definition -- coming home from AITP 2019. I should have been coming home from AITP2020 today :-(

view this post on Zulip Jannis Limperg (Mar 28 2020 at 22:23):

Thanks, I wasn't aware of this incantation. (Coq and Agda also have this feature, but the syntax is of course very different.)


Last updated: May 13 2021 at 06:15 UTC