Lemma isinclfromcoprodwithnegimage {X Y : UU} (f : X -> Y) (is : isincl f) : isincl (sumofmaps f (@pr1 _ (λ y : Y, neg (hfiber f y)))). Proof. intros. assert (noi : ∏ (x : X) (nx : negimage f), neg (paths (f x) (pr1 nx))). { intros x nx e. induction nx as [ y nhf ]. simpl in e. apply (nhf (make_hfiber _ x e)). } assert (is' : isincl (@pr1 _ (λ y : Y, neg (hfiber f y)))). { apply isinclpr1. intro y. apply isapropneg. } apply (isofhlevelfsumofmapsnoi 1 f _ is is' noi). Defined.