[Agda] What's the type of Set?

[Ulf Norell]

On Thu, Apr 29, 2010 at 3:38 PM, Chris Casinghino <
chris.casinghino at gmail.com> wrote:

> With universe polymorphism turned on, it seems that:
>
> (\ l -> Set l) : (l : Level) -> Set (suc l)
>
> But
>
> Set : Set1
>
> I guess this is just syntax sugar getting in the way of eta reduction?
>

Set doesn't a have a function type with universe polymorphism (so there's
nothing to eta contract in your example). Set l is a language construct with
the typing rule

      l : Level
-------------------------
Set l : Set (suc l)


> Agda's explicit universe polymorphism is a lot of fun to play with.
> Is it documented anywhere?
>

Not really. Universe polymorphism is still very experimental and could be
subject to change at any time.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100429/74a6fb83/attachment.html