[Agda] Formalization of Agda's universe polymorphism

[Jesper Cockx]

Hi Stefan,

As far as I know there is no such thing, unfortunately. The closest thing
is the work by Matthieu Sozeau on universe polymorphism in Coq (see
https://www.irif.fr/~sozeau/research/publications/Universe_Polymorphism_in_Coq.pdf).
However, Agda's universe polymorphism allows some more things than Coq,
such as computing universe levels from a term and having
universe-polymorphic module parameters, which do not have a solid
theoretical justification that I know of.

-- Jesper

On Wed, Jul 4, 2018 at 2:56 PM, Stefan Monnier <monnier at iro.umontreal.ca>
wrote:

> Could someone point me to some formal presentation of Agda's universe
> polymorphism, ideally an article somewhere with soundness proof or
> something like that.
>
>
>         Stefan
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180705/9483d82c/attachment.html>