proposition: Lemma algebra_cleaving_is_algebra : is_algebra algebra_cleaving_algebra_data.
proof: Proof. repeat split. - do 5 intro. refine (maponpaths (λ x, _ x a) (mor_comp F _ _) @ _). apply (comp_action A). - intros n i a. refine (_ @ pr_action A _ _). apply (maponpaths (λ f, action (A := A) f _)). apply mor_pr. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Examples.Cartesian UniMath.CategoryTheory.DisplayedCats.Examples.Sigma UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.AlgebraicTheories.Algebras UniMath.AlgebraicTheories.AlgebraMorphisms UniMath.AlgebraicTheories.AlgebraCategoryCore UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraicTheoryMorphisms UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.AlgebraicTheoryCategory