The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

On Mon, Sep 15, 2014 at 12:11:15PM -0400, Jonathan wrote:
> On 09/15/2014 10:32 AM, Hugo Herbelin wrote:
> >...
> >You would need -impredicative-set option to show that the
> >interpretation of Prop as the impredicative variant of Set satisfies
> >your axiom.
> >
> >Inductive Erasable(S : Set) : Set := erasable: S -> Erasable S.
> 
> I note that here Erasable is Set -> Set, not Set -> Prop.
> 
> >
> >Arguments erasable [S] _.
> >
> >Theorem Erasable_inj : forall {S : Set}{a b : S}, erasable a=erasable b -> 
> >a=b.
> >Proof.
> >intros * H.
> >set (f := fun (x:Erasable S) => let 'erasable y := x in y).
> >apply f_equal with (f:=f) in H.
> >assumption.
> >Qed.
> 
> But that's provable with or without -impredicative-set.

Sure, but the point is that it does not give a model of an
(impredicative) Prop satisfying your axiom if option
-impredicative-set is not set.

> (a shorter proof is just: intros * H. injection H. trivial)

Actually yes...

Hugo