[Agda] Positive but not strictly positive types

[Aaron Stump]

I have a blog post touching on some of what we were discussing:

https://queuea9.wordpress.com/2015/04/21/the-perils-of-predicativity-and-its-opposite/

Cheers,
Aaron

On 04/12/2015 05:15 AM, Thorsten Altenkirch wrote:
> I prefer to avoid black magic :-)
>
> On 12/04/2015 09:25, "Andreas Abel" <abela at chalmers.se> wrote:
>
>> Thorsten does not believe in classical ordinals so he will likely reject
>> Xu's justification.
>>
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please send it back to me, and immediately delete it.
>
> Please do not use, copy or disclose the information contained in this
> message or in any attachment.  Any views or opinions expressed by the
> author of this email do not necessarily reflect the views of the
> University of Nottingham.
>
> 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.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda