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