proposition: Lemma issurjective_to_contr {X Y : UU} (x : X) (f : X → Y) (contr : iscontr Y) : issurjective f.
proof: Proof. intro; apply hinhpr. apply(make_hfiber f x). apply proofirrelevancecontr, contr. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics