fact: Definition make_lambda_theory_data (T : algebraic_theory) (app : ∏ n f, app_ax T n f) (abs : ∏ n f, abs_ax T n f) : lambda_theory_data := T ,, app ,, abs.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.LambdaTheoryCategoryCore