The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

Hi,

I would like to encode Russell's paradox in Coq for my class, or more  
precisely Thierry's version of it (the paradox of trees). But how do I  
assume tat there is a set of all sets, or Set : Set?

The easiest would be if there were a switch to switch off size  
checking. Is there?

Ok, I could just assume that there is a set of all sets:

Variable set : Set.
Variable name : Set -> set.
Variable El : set -> Set.
Axiom reflect : forall A:Set,El (name A) = A.

but I got into trouble with this. While I can construct a function

fst : El (name { a:A | P a}) -> A.

I am having trouble with

snd : forall ap : El (name { a:A | P a}) ,P (fst ap)

Dually, there is no problem with

mk : forall a:A, (P a) -> El (name { a:A | P a})

but I also need

mkOk : forall (a:A) (p:P a) , fst (mk a p) = a

I suspect I need K (or I am just too stupid). Can anybody conform  
either? I.e. can I prove this using Coq.Logic.Eqdep or without?

I attach my Russell file with the two additional assumptions I'd like  
to eliminate.


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.

Attachment: l16-crib.v
Description: Binary data

Cheers,
Thorsten