[Agda] Universe polymorphism

[Benja Fallenstein]

On Fri, Sep 25, 2009 at 6:39 PM, Ulf Norell <ulfn at chalmers.se> wrote:
>> 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?
>
> No built-in support. You can define the Lift datatype above.

Even cooler. It sounds like this time I'll be upgrading Ubuntu as soon
as the beta comes out.

- Benja