proposition: Lemma is_limit_lambda_theory_data_disp_cat (d' : total_category D) (cone_out : ∏ u, d' --> (dob d u)) (is_cone : ∏ u v e, cone_out u · (dmor d e) = cone_out v) (algebraic_theory_arrow := limArrow L _ (make_cone (d := (mapdiagram (pr1_category D) d)) _ (λ u v e, (maponpaths pr1 (is_cone u v e))))) : pr2 d' -->[algebraic_theory_arrow] tip_lambda_theory_data_disp_cat.
proof: Proof. split; intros n f; (apply subtypePath; [ intro; repeat (apply impred_isaprop; intro); apply setproperty | ]); apply funextsec; intro i. - exact (pr12 (cone_out i) n f). - exact (pr22 (cone_out i) n f). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Limits UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraicTheoryCategory UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.AlgebraicTheoryMorphisms UniMath.AlgebraicTheories.LambdaTheoryCategoryCore UniMath.AlgebraicTheories.LambdaTheories UniMath.AlgebraicTheories.LambdaTheoryMorphisms UniMath.Combinatorics.Tuples