Lemma negProp_to_uniqueChoice P : ∏ (Q:negProp P), (isaprop P × (P ⨿ Q)) <-> iscontr (P ⨿ Q). Proof. intros [Q [j [r s]]]; simpl in *. split. * intros [i v]. exists v. intro w. induction v as [v|v]. - induction w as [w|w]. + apply maponpaths, i. + contradicts (s w) v. - induction w as [w|w]. + contradicts (s v) w. + apply maponpaths, j. * intros [c e]. split. - induction c as [c|c]. + apply invproofirrelevance; intros p p'. exact (equality_by_case (e (ii1 p) @ !e (ii1 p'))). + apply invproofirrelevance; intros p p'. contradicts (s c) p. - exact c. Defined.