<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div>For the record, this is exactly what the HoTT Agda library does (at <<a href="https://github.com/HoTT/HoTT-Agda" class="">https://github.com/HoTT/HoTT-Agda</a>>).<font color="#1666bc" class=""><br class=""><br class=""></font><blockquote type="cite" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class="">On May 30, 2015, at 4:01 PM, Kirill Elagin <<a href="mailto:kirelagin@gmail.com" class="">kirelagin@gmail.com</a>> wrote:<br class=""><blockquote type="cite" class=""></blockquote><font color="#007316" class=""><br class=""></font>Well, the problem is that the things you have in `Set` are _actually_ sets, that is, 0-types.<br class="">So what is the point of renaming?<br class=""><font color="#007316" class=""><br class=""></font>Other than that, I can’t see how this can possibly cause any serious issues.<br class="">Except for the fact that you can write just `Set`, without a level, but you can’t write just `Type`.<br class="">You also can write `Set18` and `Set₄₃` but you won’t be able to do this with `Type`.<br class=""><font color="#007316" class=""><br class=""></font>On Sat, May 30, 2015 at 10:06 PM, Sergei Meshveliani <span dir="ltr" class=""><<a href="mailto:mechvel@botik.ru" target="_blank" class="">mechvel@botik.ru</a>></span> wrote:<br class=""><font color="#007316" class=""><br class=""></font>_______________________________________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class=""><a href="https://lists.chalmers.se/mailman/listinfo/agda" class="">https://lists.chalmers.se/mailman/listinfo/agda</a><br class=""><blockquote type="cite" class=""><div class=""><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"></blockquote>People,<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"></blockquote>I consider renaming `Set' to `Type' this way:<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
</blockquote><br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"></blockquote> Type : (a : Level) → Set (suc a)<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"></blockquote> Type a = Set a<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
</blockquote><br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"></blockquote>The idea is to write `Type' everywhere instead of `Set'.<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"></blockquote>Will this work all right?<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
</blockquote><br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"></blockquote>Thanks,<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
</blockquote><br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"></blockquote>------<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"></blockquote>Sergei<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
</blockquote><br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"></blockquote>_______________________________________________<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"></blockquote>Agda mailing list<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
</blockquote><a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class="">
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank" class="">https://lists.chalmers.se/mailman/listinfo/agda</a><br class="">
</div></div></div></blockquote></div></div></blockquote></div><br class=""></body></html>