proposition: Lemma isaprop_is_algebraic_theory (T : algebraic_theory_data_cat) : isaprop (is_algebraic_theory T).
proof: Proof. repeat apply isapropdirprod; repeat (apply impred_isaprop; intro); apply setproperty. Qed.
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