The Coq mailing list

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

On Sat, Sep 13, 2014 at 06:39:20PM -0400, Jonathan wrote:
> On 09/13/2014 11:59 AM, Hugo Herbelin wrote:
> >Hi,
> >
> >On Fri, Sep 12, 2014 at 09:41:12PM -0400, Jonathan wrote:
> >>..  Are things just as bad if I
> >>limit Erasable to be over Set instead of Type?
> >In the Set-impredicative version of the Calculus of Inductive
> >Constructions, you can (relevantly) interpret Prop as impredicative
> >Set and define an injective erasable over types in Set. Up to
> >impredicativity that Prop has but Type not, this is Matthieu's claim
> >that there is a proof-relevant model of Erasable (with its restriction
> >to Set needed).
> >
> >Hugo Herbelin
> 
> So, to make sure I don't mess this up again, is all I need the following?:
> 
> Run with -impredicative-set.
> 
> Inductive Erasable(S : Set) : Prop :=
>   erasable: S -> Erasable S.
> 
> Arguments erasable [S] _.
> 
> Axiom Erasable_inj : forall {S : Set}{a b : S}, erasable a=erasable
> b -> a=b.
> 
> Or, is something more necessary?

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.

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 you don't need -impredicative-set to technically postulate your
axiom (having option -impredicative-set on does not ensure in itself
that the interpretation of Prop as the impredicative variant of Set is
sound - an analysis of the CIC rules is necessary -, nor does it
prevent introducing other axioms that would contradict this
interpretation of Prop).

Hugo