Lemma isisolatedweqf { X Y : UU } (f : X ≃ Y) (x:X) : isisolated X x -> isisolated Y (f x). Proof. intros is. unfold isisolated. intro y. induction (is (invmap f y)) as [ eq | ne ]. { apply ii1. apply pathsweq1'. assumption. } { apply ii2. intro eq. apply ne; clear ne. apply pathsweq1. assumption. } Defined.