Lemma issurjprtoimage {X Y : UU} (f : X -> Y) : issurjective (prtoimage f). Proof. intros. intro z. set (f' := prtoimage f). assert (ff: hfiber (funcomp f' (pr1image f)) (pr1 z) -> hfiber f' z) by refine (invweq (samehfibers _ _ (isinclpr1image f) z)). apply (hinhfun ff). exact (pr2 z). Defined.