[Agda] Universe polymorphism

[Ulf Norell]

On Fri, Sep 25, 2009 at 6:30 PM, Benja Fallenstein <
benja.fallenstein at gmail.com> wrote:

> Hi Ulf,
>
> >   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?


No built-in support. You can define the Lift datatype above.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20090925/348dc453/attachment.html