The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

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?

-- Jonathan