proposition: Lemma one_point_is_theory : is_algebraic_theory one_point_theory_data.
proof: Proof. use make_is_algebraic_theory. - now do 6 intro. - intros m n i f. simpl. now induction (f i). - intros n f. now induction f. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Functors UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.Algebras