Lemma homotfuntranspos2 {T : UU} (t1 t2 : T) (is1 : isisolated T t1) (is2 : isisolated T t2) : homot (funcomp (funtranspos (tpair _ t1 is1) (tpair _ t2 is2)) (funtranspos (tpair _ t1 is1) (tpair _ t2 is2))) (idfun _). Proof. intros. intro t. simpl. induction (is1 t) as [ et1t | net1t ]. - rewrite (pathsinv0 et1t). rewrite (pathsfuntransposoft1 _ _). rewrite (pathsfuntransposoft2 _ _). apply idpath. - induction (is2 t) as [ et2t | net2t ]. + rewrite (pathsinv0 et2t). rewrite (pathsfuntransposoft2 _ _). rewrite (pathsfuntransposoft1 _ _). apply idpath. + rewrite (pathsfuntransposofnet1t2 _ _ _ _ _ net1t net2t). rewrite (pathsfuntransposofnet1t2 _ _ _ _ _ net1t net2t). apply idpath. Defined.