proposition: Lemma is_limit_algebraic_theory_data_disp_cat (d' : total_category D) (cone_out : ∏ (u : vertex J), d' --> (dob d u)) (is_cone : ∏ (u v : vertex J) (e : edge u v), cone_out u · (dmor d e) = cone_out v) : pr2 d' -->[limArrow L _ (make_cone (d := (mapdiagram (pr1_category D) d)) _ (λ u v e, (maponpaths pr1 (is_cone u v e)))) ] tip_algebraic_theory_data_disp_cat.
proof: Proof. split. - intros n i. apply subtypePairEquality. { intro. repeat (apply impred_isaprop; intro). apply setproperty. } apply funextsec. intro u. exact (pr12 (cone_out u) n i). - intros m n f g. apply subtypePairEquality. { intro. repeat (apply impred_isaprop; intro). apply setproperty. } apply funextsec. intro i. exact (pr22 (cone_out i) m n f g). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Categories.HSET.Core 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.AlgebraicTheories.IndexedSetCategory UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraicTheoryMorphisms