Theorem isdecinclfromiscoproj {X Y : UU} (f : X -> Y) (is : iscoproj f) : isdecincl f. Proof. intros. set (g := (sumofmaps f (@pr1 _ (λ y : Y, neg (hfiber f y))))). set (f' := λ x : X, g (ii1 x)). assert (is' : isdecincl f') by apply (isdecinclcomp _ _ (isdecinclii1 _ _) (isdecinclfromisweq _ is)). assumption. Defined.