proposition: Lemma free_object_is_algebra : is_algebra free_object_algebra_data.
proof: Proof. use make_is_algebra. - intros m n f g a. refine (!eqtohomot (functor_comp G _ _) _ @ !_). apply (maponpaths (λ x, #G x f)). apply (φ_adj_inv_natural_postcomp (make_adjunction _ H)). - intros n i a. refine (_ @ eqtohomot (pr2 H _) _). refine (eqtohomot (functor_comp G _ _) _ @ _). apply (maponpaths (#G _)). refine (!eqtohomot (nat_trans_ax η (stnset n) _ a) i). 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