proposition: Lemma isaproptotal2 {X : UU} (P : X → UU) : isPredicate P → (∏ x y : X, P x → P y → x = y) → isaprop (∑ x : X, P x).
proof: Proof. intros HP Heq. apply invproofirrelevance. intros [x p] [y q]. induction (Heq x y p q). induction (iscontrpr1 (HP x p q)). apply idpath. Defined.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions