fact: Definition comparehomotopycompwithfunwithpathcompwithfun {X Y Z : UU} (f : X → Y) {g_1 g_2 : Y → Z} (alpha : g_1 ~ g_2) : funextfun _ _ (funhomot f alpha) = compfunwithpath f (funextfun _ _ alpha).
imports: UniMath.Foundations.All UniMath.Induction.PolynomialFunctors UniMath.CategoryTheory.Core.Functors UniMath.Induction.FunctorAlgebras_legacy