fact: Definition homottranspost2t1t1t2 {T : UU} (t1 t2 : T) (is1 : isisolated T t1) (is2 : isisolated T t2) : homot (funcomp (funtranspos (tpair _ t1 is1) (tpair _ t2 is2)) (funtranspos (tpair _ t2 is2) (tpair _ t1 is1))) (idfun _).
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom