fact: Definition funtranspos {T : UU} (t1 t2 : isolated T) : T -> T := recomplf (pr1 t1) (pr1 t2) (pr2 t1) (funtranspos0 (pr1 t1) (pr1 t2) (pr2 t2)).
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom