The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Keiko Nakata wrote:
> I hit this problem in an attempt to use Prop as impredicative Set. 
> Having learned that the use of Set-valued nat confused me, 
> I wonder if I can avoid them. 
> Namely, is there a Prop-valued equivalent to nat and Z?
>   

While I can't give you a very formal answer, I can say this, as someone 
who has spent a lot of time trying to do crafty things with 
impredicativity: you can rarely if ever switch seamlessly from 
predicative to impredicative computation.  The elimination restrictions 
really do in practice keep you from doing some common computational 
things impredicatively.

Perhaps you can give us more background on your application, so that we 
can give more targeted advice.