<div dir="ltr"><div><div><div><div>Well, the problem is that the things you have in `Set` are _actually_ sets, that is, 0-types.<br></div>So what is the point of renaming?<br><br></div>Other than that, I can’t see how this can possibly cause any serious issues.<br></div>Except for the fact that you can write just `Set`, without a level, but you can’t write just `Type`.<br></div>You also can write `Set18` and `Set₄₃` but you won’t be able to do this with `Type`.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, May 30, 2015 at 10:06 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">People,<br>
I consider renaming `Set' to `Type' this way:<br>
<br>
Type : (a : Level) → Set (suc a)<br>
Type a = Set a<br>
<br>
The idea is to write `Type' everywhere instead of `Set'.<br>
Will this work all right?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>