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