<div dir="ltr"><div>Hi Stefan,</div><div><br></div><div>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 <a href="https://www.irif.fr/~sozeau/research/publications/Universe_Polymorphism_in_Coq.pdf">https://www.irif.fr/~sozeau/research/publications/Universe_Polymorphism_in_Coq.pdf</a>). 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.</div><div><br></div><div>-- Jesper<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Jul 4, 2018 at 2:56 PM, Stefan Monnier <span dir="ltr"><<a href="mailto:monnier@iro.umontreal.ca" target="_blank">monnier@iro.umontreal.ca</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Could someone point me to some formal presentation of Agda's universe<br>
polymorphism, ideally an article somewhere with soundness proof or<br>
something like that.<br>
<br>
<br>
        Stefan<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>