Definition invcutonweq {T : UU} (t : T) (is : isisolated T t) (t'w : isolated T × (compl T t ≃ compl T t)) : T ≃ T := weqcomp (weqrecomplf t t is is (pr2 t'w)) (weqtranspos t (pr1 (pr1 t'w)) is (pr2 (pr1 t'w))).