The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 05/28/2016 10:26 PM, Jason Gross wrote:

Have you considered LEM on hProps?
  forall P, (forall x y : P, x = y) -> P \/ ~P
Together with propositional truncation / quotient types, this may give you
want you want.  (I think these are similar to your irrelevant_sibling; you
do:
  Module Export Trunc.
    Private Inductive PropTrunc A := tr : A -> PropTrunc A.
    Axiom PropTrunc_trunc : forall {A} (x y : PropTrunc A), x = y.
    Definition Trunc_ind {A}
      (P : PropTrunc A -> Type) {Pt : forall x y, P x = P y}
    : (forall a, P (tr a)) -> (forall aa, P aa)
    := (fun f aa => match aa with tr a => fun _ => f a end Pt).
  End Trunc.
)
Does this do what you want?

It turns out that the Prop version of this Private trick, plus the proof relevance I'm working with, is inconsistent:

Module Export TruncP.
  Private Inductive PropTruncP (A : Prop) : Prop := tr : A -> PropTruncP A.
  Arguments tr [A] _.
  Axiom PropTruncP_trunc : forall {A : Prop} (x y : PropTruncP A), x = y.
  Definition TruncP_ind {A}
    (P : PropTruncP A -> Prop) {Pt : forall x y, P x = P y}
  : (forall a, P (tr a)) -> (forall aa, P aa)
    := (fun f aa => match aa with tr a => fun _ => f a end Pt).
End TruncP.

Inductive Erasable(A : Set) : Prop := erasable: A -> Erasable A.
Arguments erasable [A] _.
Axiom Erasable_inj : forall {A : Set}{a b : A}, erasable a=erasable b -> a=b. (*proof relevance*)

Inductive Foo : Prop := foo: bool -> Foo.

Definition foo2erasable(f : Foo) : Erasable bool :=
  match f with
    foo x => erasable x
  end.

Definition trunc_foo2erasable(f : PropTruncP Foo) : Erasable bool :=
  @TruncP_ind Foo (fun _ => Erasable bool) (fun _ _ => eq_refl) foo2erasable f.

Theorem inconsistent: False.
Proof.
  assert (tr (foo true) = tr (foo false)) as H by apply PropTruncP_trunc.
  apply f_equal with (f := trunc_foo2erasable) in H.
  cbv in H.
  apply Erasable_inj in H.
  discriminate.
Qed.

-- Jonathan