[Agda] Difference between two datatypes

[Samuel Bronson]

On 6/19/08, Nils Anders Danielsson <nils.anders.danielsson at gmail.com> wrote:

> Set and Set1 are different universes. Note, for instance, that you can
> form the type X (X a), but not Y (Y a). It is generally a good idea to
> avoid Set1 as much as possible, since other types (for instance in
> libraries) are often parameterised on Sets, not Set1s.

I hope that gets fixed soonish... it's terribly annoying...