[Agda] More universe polymorphism

[Dan Doel]

On Fri, Jun 28, 2013 at 9:13 PM, Guillaume Brunerie <
guillaume.brunerie at gmail.com> wrote:

> (2) Yes, Agda’s universe polymorphism is more expressive than MLTT
> with countably many universes. But as I said above you can see such
> large types and terms as living in the meta-level. In MLTT with
> countably many universes you can still define your f as an external
> macro (or notational convention), but in Agda this is actually part of
> the language.
>

Oh, I forgot to mention this in my last e-mail....

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:

     http://code.haskell.org/~dolio/agda-share/universes/html/Hierarchy.html

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.

It's probably also feasible to model your ordinal-like level type, but I
haven't tried it out yet.

-- Dan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130628/640e93db/attachment.html