Definition weqtranspos0 {T : UU} (t1 t2 : T) : isisolated T t1 -> isisolated T t2 -> compl T t1 ≃ compl T t2. Proof. intros is1 is2. simple refine (weq_iso (funtranspos0 t1 t2 is2) (funtranspos0 t2 t1 is1) _ _). - intro x. apply (homottranspos0t2t1t1t2 t1 t2 is1 is2). - intro x. apply (homottranspos0t2t1t1t2 t2 t1 is2 is1). Defined.