fact: Definition immisalghomotopy {X : UU} {s_X : P X → X} {Y : UU} {s_Y : P Y → Y} (f : X → Y) (sigma_f : s_X ;; f ~ # P f ;; s_Y) (g : X → Y) (sigma_g : s_X ;; g ~ # P g ;; s_Y) (alpha : f ~ g) : isalgmaphomotopy f sigma_f g sigma_g alpha → homotcomp (funhomot s_X alpha) (sigma_g) = (homotcomp (sigma_f) (homotfun (P_2_h alpha) s_Y)).
imports: UniMath.Foundations.All UniMath.Induction.PolynomialFunctors UniMath.CategoryTheory.Core.Functors UniMath.Induction.FunctorAlgebras_legacy