The Coq mailing list

[darktenaibre <darktenaibre AT isomorphis.me>]

On 04/24/2016 03:00 AM, Jonathan Leivent wrote:
> 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
I do not think so, taking T := P * bool and f := fun x => x , true.

Now that I thought more about it, even my (weaker I think) proposition 
is bogus in this respect. I conjecture you could take T := P * Type and 
then try to use the equality P * Type = Q for some (Q : Prop) and 
exhibit some sort of (Type : Type) paradox to prove false, thus also 
proving proof_irrelevance from that. But no certainties so far.