Theorem isdecinclhomot {X Y : UU} (f g : X -> Y) (h : ∏ x : X, paths (f x) (g x)) (is : isdecincl f) : isdecincl g. Proof. intros. intro y. apply (isdecpropweqf (weqhfibershomot f g h y) (is y)). Defined.