fact: Definition make_algebra_morphism {T : algebraic_theory} {A A' : algebra T} (F : A → A') (H : ∏ n f a, mor_action_ax (identity T) F (@action T A) (@action T A') n f a) : algebra_morphism A A' := F ,, H ,, tt.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Combinatorics.StandardFiniteSets UniMath.CategoryTheory.Core.Functors UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.Algebras UniMath.AlgebraicTheories.AlgebraCategoryCore