Theorem isdecinclf {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (isg : isincl g) (isgf : isdecincl (λ x : X, g (f x))) : isdecincl f. Proof. intros. intro y. set (gf := λ x : _, g (f x)). assert (ww : weq (hfiber f y) (hfiber gf (g y))) by (apply (samehfibers f g); assumption). apply (isdecpropweqb ww (isgf (g y))). Defined.