fact: Definition homottranspos0t2t1t1t2 {T : UU} (t1 t2 : T) (is1 : isisolated T t1) (is2 : isisolated T t2) : funtranspos0 t2 t1 is1 ∘ funtranspos0 t1 t2 is2 ~ idfun _.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom