proposition: Lemma issurjective_sumofmaps_1 {X A B : UU} (f : A -> X) (g : B -> X) (fsurjective : issurjective f) : issurjective (sumofmaps f g).
proof: Proof. intro x. use(hinhfun _ (fsurjective x)). intro ffiber; apply coprodofhfiberstohfiber. exact(inl ffiber). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics