[Agda] What's the type of Set?

[Nils Anders Danielsson]

On 2010-04-29 16:38, Chris Casinghino wrote:
> With universe polymorphism turned on, it seems that:
> 
> (\ l -> Set l) : (l : Level) -> Set (suc l)
> 
> But
> 
> Set : Set1

The expression "Set" is syntactic sugar for "Set zero" (assuming that
the zeroth level is called zero).

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

Most features added in the 2.2 series are documented in the release
notes:

  http://code.haskell.org/Agda/doc/release-notes/

-- 
/NAD