[Agda] Type a = Set a

[Kirill Elagin]

Well, the problem is that the things you have in `Set` are _actually_ sets,
that is, 0-types.
So what is the point of renaming?

Other than that, I can’t see how this can possibly cause any serious issues.
Except for the fact that you can write just `Set`, without a level, but you
can’t write just `Type`.
You also can write `Set18` and `Set₄₃` but you won’t be able to do this
with `Type`.

On Sat, May 30, 2015 at 10:06 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> People,
> I consider renaming `Set' to `Type' this way:
>
>   Type : (a : Level) → Set (suc a)
>   Type a = Set a
>
> The idea is to write `Type' everywhere instead of `Set'.
> Will this work all right?
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150531/26f90d3f/attachment.html