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