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