proposition: Lemma projections_theory_algebra_is_algebra (A : hSet) : is_algebra (projections_theory_algebra_data A).
proof: Proof. now use make_is_algebra; repeat intro. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Functors UniMath.Combinatorics.StandardFiniteSets UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.Algebras