[Agda] Universe polymorphism

[Benja Fallenstein]

Hi Ulf,

On Fri, Sep 25, 2009 at 6:17 PM, Ulf Norell <ulfn at chalmers.se> wrote:
> The development version now has (very experimental) support for
> (non-uniform) universe
> polymorphism.

Cool! :-)

>   At present there is no way to lift types from one level to another, that
>   is, there is no function
>     lift : {i : Level} -> Set i -> Set (suc i)
>   This is likely to change at some point.

Does that mean that doing it manually using levels in data
declarations is not / not yet possible? I.e.,

data Lift {i : Level} (X : Set i) : (Set (suc i)) where
  lift : X -> Lift X

Or does it just mean there's no built-in support? (Unfortunately I'm
stuck on GHC 6.8 for the moment, so I can't try myself just yet -- I'm
hoping 6.10 will be in Ubuntu 9.10, though I haven't figured out yet
if it is...)

Thanks,
- Benja