The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Consider this weak version of proof irrelevance:

Definition proof_uninformativeness := forall (P : Prop)(S : Set)(f : P 
-> S)(p1 p2 : P), f p1 = f p2.

I think this is true in Coq (by design), but I don't know if it can be 
proven.  Probably not ...?

Also, are there use cases of proof irrelevance where this weaker version 
isn't sufficient?  I suspect there might be in cases where Set isn't big 
enough.  If so, is there a way to quantify Types that are not Props in 
Coq, so one could write:

Definition proof_uninformativeness' := forall (P : Prop)(T : Type)(f : P 
-> T)(p1 p2 : P), notprop T -> f p1 = f p2.

And if that's possible (I suspect it isn't), would that cover all 
interesting use cases of proof irrelevance?

-- Jonathan