proposition: Lemma free_object_algebra_is_morphism (n : nat) (t : free_object_theory n) (a : stn n → free_object_algebra c) : mor_action_ax (identity free_object_theory) (free_object_algebra_morphism_data) (@action _ (free_object_algebra c)) (@action _ (free_object_algebra c')) n t a.
proof: Proof. refine (!eqtohomot (functor_comp G _ _) _ @ !_). apply (maponpaths (λ x, #G x t)). apply (φ_adj_inv_natural_postcomp (make_adjunction _ H)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Adjunctions.Core UniMath.Combinatorics.StandardFiniteSets UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraCategoryCore UniMath.AlgebraicTheories.Algebras UniMath.AlgebraicTheories.AlgebraMorphisms UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore