[Agda] What's the type of Set?

[Chris Casinghino]

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?

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

--Chris