proposition: Lemma pr1_issurjective {X : UU} {P : X -> UU} : (∏ x : X, ∥ P x ∥) -> issurjective (pr1 : (∑ x, P x) -> X).
proof: Proof. intros ne x. simple refine (hinhuniv _ (ne x)). intros p. apply hinhpr. exact ((x,,p),,idpath _). Defined.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Sets