The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 04/23/2016 10:39 PM, Gabriel Scherer wrote:
> f is injective iff (f p = f q) implies (p = q). This is compatible with
> proof-irrelevance. In particular, all functions whose domain is in a
> proof-irrelevant Prop are injective.

But, proof irrelevance is not compatible with injectivity of a 
Prop-typed function with non-Prop-typed args.  Which is why Coq doesn't 
define Prop constructors to be injective.  Unfortunately, I need a 
single Prop constructor with a single Set-typed arg to be injective (via 
an axiom), but would otherwise like some aspects of proof irrelevance.  
But, thanks to this discussion, I'm convinced this attempt isn't going 
to work.

Thanks,
-- Jonathan.

> On Sat, Apr 23, 2016 at 10:10 PM, Jonathan Leivent 
> <jonikelee AT gmail.com>
> wrote:
>
> > Sigh... there's got to be a version that "works" - that captures Coq's
> > uninformative Prop concept, yet is weaker than proof irrelevance.  Is it
> > enough to restrict T to bool? :
> >
> > Definition proof_uninformativeness := forall (P : Prop)(f : P -> bool)(p1
> > p2 : P), f p1 = f p2.
> >
> > What I'm trying to do is to work in a context where proof irrelevance is
> > inconsistent (because I need injectivity of some props), yet one can still
> > have its benefits.  So, I would like to keep proofs relevant to other
> > proofs, but not to non-Prop types somehow...
> >
> > -- Jonathan