fact: Definition make_algebraic_theory_data (T : nat → hSet) (pr : ∏ n i, pr_ax T n i) (comp : ∏ m n f g, comp_ax T m n f g) : algebraic_theory_data := T ,, pr ,, comp.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.Combinatorics.Tuples