[Agda] What's the type of Set?

[Chris Casinghino]

> 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)

Thanks, this makes sense.  I had guessed that Agda had the typing rule:


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

Instead.  Are you aware of any reason to pick one over the other?

--Chris