The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

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?  That would be somewhat limiting, but 
maybe still sufficiently useful.  Or, if there was a way to limit it to 
non-universe instances of Type?

Still - the proof (in Daniel Shepler's response) that it is incompatible 
with specific proof irrelevance is also upsetting - and that would 
remain even if limited to Set.  Although I haven't yet required any 
variety of proof irrelevance.

Well, either I have to hope reality is sufficiently paraconsistent, or 
investigate an alternative erasability mechanism.  Maybe the one Daniel 
Shepler is suggesting is suitable.

Or switch to Idris.

-- Jonathan