Lift a type to a higher universe

Stream: new members

[Jannis Limperg]

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.)

[Reid Barton]

ulift

[Jannis Limperg]

Thanks!

[Kevin Buzzard]

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 :-(

[Jannis Limperg]

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