[Agda] More universe polymorphism
dan.doel at gmail.com
Sat Jun 29 03:45:14 CEST 2013
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:
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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda