[Agda] Universe polymorphism in the standard library

[Edward Kmett]

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. ;)

-Edward Kmett

On Thu, Nov 19, 2009 at 3:09 PM, Thorsten Altenkirch <txa at cs.nott.ac.uk>wrote:

> Hi,
>
> 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.
>
> As a stop gap I am using
> {-# OPTIONS --type-in-type #-}
>
> It is usually easy to see wether your definitions can be stratified.
>
> Cheers,
> Thorsten
>
> On 19 Nov 2009, at 18:41, Edward Kmett wrote:
>
> When did universe polymorphism sneak in?
>
> The lack of it was the reason I stopped using Agda!
>
> -Edward Kmett
>
> On Thu, Nov 19, 2009 at 1:33 PM, Luke Palmer <lrpalmer at gmail.com> wrote:
>
>> I have been diving into Agda recently, and have a decent amount of
>> tuits.  I notice that a decent amount of the standard library is not
>> using universe polymorphism.  Is there a reason for this, or is it
>> just that nobody has got a round tuit?  I'd be happy to start
>> converting things if the latter.
>>
>> Luke
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>  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.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091119/544696a6/attachment.html