The Coq mailing list

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

Hi,

On Fri, Sep 12, 2014 at 09:41:12PM -0400, Jonathan wrote:
> On 09/12/2014 07:59 PM, Robert Dockins wrote:
> >
> >You can get this from the Hurkens paradox; see below.
> >
> >Cheers,
> >   Rob
> >
> >--------------------------------------
> >
> >
> >Require Hurkens.
> >
> >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.
> >
> >
> >Definition er_out (X:Erasable Prop) : Prop
> >    := exists P, X = @erasable Prop P /\ P.
> >
> >Theorem inconsistent : False.
> >Proof.
> >   apply (Hurkens.paradox (Erasable Prop) (@erasable Prop) er_out).
> >
> >   intros.
> >   destruct H as [P [H1 H2]].
> >   apply Erasable_inj in H1.
> >   subst A. trivial.
> >
> >   red; intros.
> >   exists A; split; auto.
> >Qed.
> >
> >Check inconsistent.
> >Print Assumptions inconsistent.
> >
> 
> I needed to add Import Hurkens.NoRetractFromSmallPropositionToProp.
> and use "paradox" unqualified, for some reason - but otherwise it
> does work (I'm using a trunk version).  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