<div dir="ltr">On Fri, Jun 28, 2013 at 9:13 PM, Guillaume Brunerie <span dir="ltr"><<a href="mailto:guillaume.brunerie@gmail.com" target="_blank">guillaume.brunerie@gmail.com</a>></span> wrote:<br><div class="gmail_extra">
<div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">(2) Yes, Agda’s universe polymorphism is more expressive than MLTT<br>
with countably many universes. But as I said above you can see such<br>
large types and terms as living in the meta-level. In MLTT with<br>
countably many universes you can still define your f as an external<br>
macro (or notational convention), but in Agda this is actually part of<br>
the language.<br></blockquote><div><br>Oh, I forgot to mention this in my last e-mail....<br><br>It's quite easy to model Agda-like universe polymorphism _in Agda_, without universe polymorphism, thanks to induction-recursion. Here's an example of something similar here:<br>
<br> <a href="http://code.haskell.org/~dolio/agda-share/universes/html/Hierarchy.html">http://code.haskell.org/~dolio/agda-share/universes/html/Hierarchy.html</a><br><br>I added a definition at the end that corresponds to (i : Level) -> Set i. The bottom universe has a type of levels and it can be used in the Pi of the top universe to write universe polymorphic types.<br>
<br>It's probably also feasible to model your ordinal-like level type, but I haven't tried it out yet.<br><br>-- Dan<br></div></div></div></div>