Theorem isisolateddecinclf {X Y : UU} (f : X -> Y) (x : X) : isdecincl f -> isisolated X x -> isisolated Y (f x). Proof. intros isf isx. assert (is' : ∏ y : Y, isdecincl (d1g f y x)). { intro y. intro xe. set (w := ezweq2g f x xe). apply (isdecpropweqf w (isdecproppathstoisolated X x isx _)). } assert (is'' : ∏ y : Y, isdecprop ((f x) = y)) by (intro; apply (isdecpropfromdecincl _ (is' y) (isf y))). intro y'. apply (pr1 (is'' y')). Defined.