[Agda] Difference between two datatypes

[Nils Anders Danielsson]

On Thu, Jun 19, 2008 at 4:23 PM, Sean Leather <sean.leather at gmail.com> wrote:
>
> What are the differences (if any) between the following two datatypes?
>
> data X (a : Set) : Set where
>   x : a -> X a
>
> data Y : Set -> Set1 where
>   y : {a : Set} -> a -> Y a

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.

-- 
/NAD