Theorem iscoprojfromisdecincl {X Y : UU} (f : X -> Y) (is : isdecincl f) : iscoproj f. Proof. intros. set (p := sumofmaps f (@pr1 _ (λ y : Y, neg (hfiber f y)))). assert (is' : isincl p). { apply isinclfromcoprodwithnegimage. apply (isdecincltoisincl _ is). } unfold iscoproj. intro y. induction (pr1 (is y)) as [ h | nh ]. - induction h as [ x e ]. induction e. change (f x) with (p (ii1 x)). apply iscontrhfiberofincl. assumption. - change y with (p (ii2 (make_negimage _ y nh))). apply iscontrhfiberofincl. assumption. Defined.