Definition homottranspost2t1t1t2 {T : UU} (t1 t2 : T) (is1 : isisolated T t1) (is2 : isisolated T t2) : homot (funcomp (funtranspos (tpair _ t1 is1) (tpair _ t2 is2)) (funtranspos (tpair _ t2 is2) (tpair _ t1 is1))) (idfun _). Proof. intros. intro t. unfold funtranspos. rewrite (homotrecomplfcomp t1 t2 t1 is1 is2 _ _ t). set (e := homotrecomplfhomot t1 t1 is1 _ (idfun _) (homottranspos0t2t1t1t2 t1 t2 is1 is2) t). set (e' := homotrecomplfidfun t1 is1 t). apply (pathscomp0 e e'). Defined.