I had started by using --type-in-type, but I backed off, mainly because I was never entirely sure that Hurkens'/Girard's paradox wasn't lurking in any of my proofs. It kind of defeated the purpose of doing everything so rigorously. ;)<br>
<br>-Edward Kmett<br><br><div class="gmail_quote">On Thu, Nov 19, 2009 at 3:09 PM, Thorsten Altenkirch <span dir="ltr"><<a href="mailto:txa@cs.nott.ac.uk">txa@cs.nott.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div style="word-wrap: break-word;">Hi,<div><br></div><div>Ulf has got an experimental implementation of universe polymorphism. However, I'd think it is too early to reimplement the whole library based on this.</div><div>
<br></div><div>As a stop gap I am using </div><div><div>{-# OPTIONS --type-in-type #-}</div></div><div><br></div><div>It is usually easy to see wether your definitions can be stratified. </div><div><br></div><div>Cheers,</div>
<div>Thorsten</div><div><div></div><div class="h5"><div><br></div><div><div><div>On 19 Nov 2009, at 18:41, Edward Kmett wrote:</div><br><blockquote type="cite">When did universe polymorphism sneak in? <br><br>The lack of it was the reason I stopped using Agda!<br>
<br>-Edward Kmett<br><br><div class="gmail_quote">On Thu, Nov 19, 2009 at 1:33 PM, Luke Palmer <span dir="ltr"><<a href="mailto:lrpalmer@gmail.com" target="_blank">lrpalmer@gmail.com</a>></span> wrote:<br> <blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
I have been diving into Agda recently, and have a decent amount of<br> tuits. I notice that a decent amount of the standard library is not<br> using universe polymorphism. Is there a reason for this, or is it<br> just that nobody has got a round tuit? I'd be happy to start<br>
converting things if the latter.<br> <br> Luke<br> _______________________________________________<br> Agda mailing list<br> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br> _______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div></div></div></div><br>
<p>
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
</p>
</blockquote></div><br>