The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Indeed, if you have constructive definite description (which is, I think, the same as assuming the elim rule for hProp), this is doable:

Set Implicit Arguments.

Require Import Description.

Lemma this_is_true : forall p q : Prop, (forall x y : p, x = y) -> (forall x y : q, x = y) -> p \/ q -> ~ (p /\ q) -> {p} + {q}.

Proof.

  intros p q p_irr q_irr H H0.

  refine (@proj1_sig _ (fun _ => True) _).

  apply constructive_definite_description.

  destruct H as [x|x];

    [ (exists (left x))

    | (exists (right x)) ];

    split; trivial;

    intros [y|y] [];

    f_equal;

    first [ apply p_irr

          | apply q_irr

          | destruct (H0 (conj x y))

          | destruct (H0 (conj y x)) ].

Defined.

-Jason

On Sun, Dec 8, 2013 at 2:58 PM, Andrej Bauer <andrej.bauer AT andrej.com> wrote:

I thought so, and I do not see how to play a trick with singleton
elimination to get it done (that's the only chance to eliminate from
Prop into Type, as far as I know). In homotopy type theory this should
be doable. There \/ is interpreted as the propositional truncation of
+.

With kind regards,

Andrej