The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 09/12/2014 05:44 PM, Greg Morrisett wrote:
> Uhm, I'm a little worried about this idea of selective proof
> irrelevance and the interaction with an injectivity axiom
> for some nat -> Prop constructor.  This is exactly what we
> wanted in Ynot, but I didn't see how to do it safely...
>
> Can you say more Jonathan?
>
> -Greg

    Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.

So, that certainly won't mix with:


   Inductive Erasable(A : Type) : Prop :=
      erasable: A -> Erasable A.

   Arguments erasable [A] _.

   Axiom Erasable_inj : forall {A : Type}{a b : A}, erasable a=erasable
   b -> a=b.


A specific Prop P other than Erasable irrelevance:

Axiom P_irrelevance : forall (p1 p2:P), p1 = p2.


Maybe there is a problem here?  I will try to create a contradiction in 
this case, using a Prop that is identical in structure to Erasable, but 
just not itself Erasable - that actually does look possible...

-- Jonathan