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