proposition: Lemma algebra_mor_comp {T : algebraic_theory} {A A' A'' : algebra T} (F : algebra_morphism A A') (F' : algebra_morphism A' A'') : algebra_morphism_to_function (F · F') = funcomp F F'.
proof: Proof. refine (pr1_transportf (B := λ _, A → A'') _ _ @ _). exact (maponpaths (λ z, z _) (transportf_const _ _)). Qed.
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