proposition: Lemma pathsfuntransposoft2 {T : UU} (t1 t2 : T) (is1 : isisolated T t1) (is2 : isisolated T t2) : paths (funtranspos (tpair _ t1 is1) (tpair _ t2 is2) t2) t1.
proof: Proof. intros. unfold funtranspos. simpl. unfold funtranspos0. unfold recomplf. unfold coprodf. unfold invmap. unfold weqrecompl. unfold recompl. simpl. unfold invrecompl. induction (is1 t2) as [ et1t2 | net1t2 ]. - apply (pathsinv0 et1t2). - simpl. induction (is2 t2) as [ et2t2 | net2t2 ]. + induction (is2 t1) as [ et2t1 | net2t1 ]. * induction (net1t2 (pathscomp0 (pathsinv0 et2t1) et2t2)). * simpl. apply idpath. + induction (net2t2 (idpath _)). Defined.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom