proposition: Lemma issurjective_coprodf {X Y W Z : UU} {f : X → W} {g : Y → Z} (fsurjective : issurjective f) (gsurjective : issurjective g) : issurjective (coprodf f g).
proof: Proof. red; apply coprod_rect. - intro w. apply(hinhfun (weqhfibercoprodf1 f g w)). exact(fsurjective w). - intro z. apply(hinhfun (weqhfibercoprodf2 f g z)). exact(gsurjective z). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics