Lemma issurjective_totalfun {X : UU} (P Q : X → UU) (f : ∏ (x : X), P x → Q x) (fsurjective : ∏ (x : X), issurjective (f x)) : issurjective (totalfun P Q f). Proof. intros [x qx]. use(hinhfun _ (fsurjective x qx)). intros [px pathpx]. use make_hfiber. - exact(x ,, px). - exact(pair_path_in2 Q pathpx). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.