Theorem weqtranspos {T : UU} (t1 t2 : T) (is1 : isisolated T t1) (is2 : isisolated T t2) : T ≃ T. Proof. intros. set (f := funtranspos (tpair _ t1 is1) (tpair _ t2 is2)). set (g := funtranspos (tpair _ t2 is2) (tpair _ t1 is1)). split with f. assert (egf : ∏ t : T, paths (g (f t)) t) by (intro; refine (homottranspost2t1t1t2 _ _ _ _ _)). assert (efg : ∏ t : T, paths (f (g t)) t) by (intro; refine (homottranspost2t1t1t2 _ _ _ _ _)). apply (isweq_iso _ _ egf efg). Defined.