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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.