[Agda] A plea for Set:Set

[Thorsten Altenkirch]

On 13 May 2008, at 22:37, Samuel Bronson wrote:

> On Tue, May 13, 2008 at 3:43 PM, Nils Anders Danielsson
> <nils.anders.danielsson at gmail.com> wrote:
>> The flag turns off the universe check when you define data types and
>> record types. However, Set1 still does not match Set.
>
> What is the price for this?

You have to pay the equivalent of EUR 1.50 into the Russell Memorial  
Fund, each time you use it. For details see
http://en.wikipedia.org/wiki/Russell%27s_paradox

:-)

Thorsten

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.