The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

AUGER Cédric a écrit :
> I may be wrong, but there is also cardinal impossibility for that
> isomorphism:
>
> cnat is a lot bigger than nat

it depends on the model you have in mind. If you interpret types has the 
set of closed lambda terms (modulo conversion) of that type, then cnat 
*is* isomorphic to nat.
Bear in mind that polymorphism cannot be interpreted set-theoretically 
(as shown by Reynolds): cnat is not the set of functions that take as 
input a set, an element of that set and a function on that set. This 
would be paradoxical in set-theory, since you end up with a set of all 
sets (even if you erase the set argument).

> ... since for each real x, there exists a cnat c such that "c
> real 0 _ = x"

I can't see how this could hold in the lambda term model above (if I 
understand your statement correctly).

So, to me, there is no cardinal impossibility, which would be very 
unfortunate since it would invalidate any extentional model of Coq.

Bruno Barras.