Definition homottranspos0t2t1t1t2 {T : UU} (t1 t2 : T) (is1 : isisolated T t1) (is2 : isisolated T t2) : funtranspos0 t2 t1 is1 ∘ funtranspos0 t1 t2 is2 ~ idfun _. Proof. intros. intro x. unfold funtranspos0. simpl. induction x as [ t net1 ]; simpl. induction (is2 t) as [ et2 | net2 ]. - induction (is2 t1) as [ et2t1 | net2t1 ]. + induction (net1 (pathscomp0 (pathsinv0 et2t1) et2)). + simpl. induction (is1 t1) as [ e | ne ]. * induction (is1 t2) as [ et1t2 | net1t2 ]. {induction (net2t1 (pathscomp0 (pathsinv0 et1t2) e)). } {apply (invmaponpathsincl _ (isinclpr1compl _ _)). simpl. exact et2. } * induction (ne (idpath _)). - simpl. induction (is1 t) as [ et1t | net1t ]. + induction (net1 et1t). + apply (invmaponpathsincl _ (isinclpr1compl _ _)). simpl. apply idpath. Defined.