Lemma issurjective_dirprodf {X Y U W} {f : X → U} {g : Y → W} (fsurjective : issurjective f) (gsurjective : issurjective g) : issurjective (dirprodf f g). Proof. intros [u w]. use(hinhfun2 _ (fsurjective u) (gsurjective w)). intros ffiber gfiber. use make_hfiber. - exact(hfiberpr1 f u ffiber ,, hfiberpr1 g w gfiber). - apply dirprodeq ; apply hfiberpr2. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.