proposition: Lemma pathsfuntransposoft1 {T : UU} (t1 t2 : T) (is1 : isisolated T t1) (is2 : isisolated T t2) : paths (funtranspos (tpair _ t1 is1) (tpair _ t2 is2) t1) t2.
proof: Proof. intros. unfold funtranspos. rewrite (pathsrecomplfxtoy t1 t2 is1 _). apply idpath. Defined.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom