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