fact: Definition fiberwise2cellto2cellalt {XX YY: algebra_ob P} (ff gg : algebra_mor P XX YY) (e: pr1 ff = pr1 gg) : isalg2cell ff gg e → isalg2cellalt ff gg e.
imports: UniMath.Foundations.All UniMath.Induction.PolynomialFunctors UniMath.CategoryTheory.Core.Functors UniMath.Induction.FunctorAlgebras_legacy