fact: Definition is_algebraic_theory (T : algebraic_theory_data_cat) : UU := (∏ l m n f_l f_m f_n, comp_comp_ax T l m n f_l f_m f_n) × (∏ m n i f, pr_comp_ax T m n i f) × (∏ n f, comp_pr_ax T n f).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.Combinatorics.StandardFiniteSets UniMath.AlgebraicTheories.IndexedSetCategory