Lemma pathsfuntransposofnet1t2 {T : UU} (t1 t2 : T) (is1 : isisolated T t1) (is2 : isisolated T t2) (t : T) (net1t : t1 != t) (net2t : t2 != t) : paths (funtranspos (tpair _ t1 is1) (tpair _ t2 is2) t) t. Proof. intros. unfold funtranspos. simpl. unfold funtranspos0. unfold recomplf. unfold coprodf. unfold invmap. unfold weqrecompl. unfold recompl. simpl. unfold invrecompl. induction (is1 t) as [ et1t | net1t' ]. - induction (net1t et1t). - simpl. induction (is2 t) as [ et2t | net2t' ]. induction (net2t et2t). simpl. apply idpath. Defined.