Definition weqrecomplf {X Y : UU} (x : X) (y : Y) (isx : isisolated X x) (isy : isisolated Y y) (w : (compl X x) ≃ (compl Y y)) : X ≃ Y := weqcomp (weqcomp (invweq (weqrecompl X x isx)) (weqcoprodf w (idweq unit))) (weqrecompl Y y isy).