proposition: Lemma issurjective_dirprodf {X Y U W} {f : X → U} {g : Y → W} (fsurjective : issurjective f) (gsurjective : issurjective g) : issurjective (dirprodf f g).
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics