The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 04/23/2016 08:41 PM, darktenaibre wrote:
> Ah, that notprop predicate prevents this stupid observation though. 
> You can certainly write something like (fun T => forall P : Prop, ~ 
> (@eq Type P T)) which will easily block the previous proof, but it's 
> probably unusable this way. I do not have any idea for a clever 
> solution to this problem though.
> On 04/24/2016 02:32 AM, darktenaibre wrote:
> > On 04/24/2016 02:21 AM, Jonathan Leivent wrote:
> > > Definition proof_uninformativeness := forall (P : Prop)(S : Set)(f : 
> > > P -> S)(p1 p2 : P), f p1 = f p2. 
> > Hi,
> > If you take f:=id, isn't it just proof irrelevance ?
> >
> >
> > Lemma proof_uninformativeness_irrelevance : proof_uninformativeness 
> > -> forall (P : Prop) (p q : P), p = q.
> >   intros pu P; apply pu.
> > Qed.

Oops - my (embarrassing) mistake having Prop not be a subtype of Set. :-[

So, there would need to be some usable notprop predicate.
Hmm... maybe types having at least 2 distinguished instances are 
sufficient? :

Definition distinguished(T : Type) := exists (a b : T), a <> b.

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

Is this a suitable replacement for all interesting use cases of proof 
irrelevance?

-- Jonathan