Theorem isdecinclg {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (isf : isweq f) (isgf : isdecincl (λ x : X, g (f x))) : isdecincl g. Proof. intros. intro z. set (gf := λ x : X, g (f x)). assert (w : (hfiber gf z) ≃ (hfiber g z)). { split with (hfibersgftog f g z). intro ye. assert (ww : weq (hfiber f (pr1 ye)) (hfiber (hfibersgftog f g z) ye)) by apply ezweqhf. apply (iscontrweqf ww (isf (pr1 ye))). } apply (isdecpropweqf w (isgf z)). Defined.