proposition: Lemma is_limit_presheaf_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) : pr2 d' -->[limArrow L _ (make_cone (d := (mapdiagram (pr1_category D) d)) _ (λ u v e, (maponpaths pr1 (is_cone u v e)))) ] tip_presheaf_data_disp_cat.
proof: Proof. intros m n f g. apply subtypePairEquality. { intro. repeat (apply impred_isaprop; intro). exact (setproperty _ _ _). } apply funextsec. intro i. exact (pr2 (cone_out i) m n f g). 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.Examples.Cartesian UniMath.CategoryTheory.DisplayedCats.Examples.Sigma UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Limits UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Terminal UniMath.Combinatorics.StandardFiniteSets UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.AlgebraicTheoryCategory UniMath.AlgebraicTheories.AlgebraicTheoryMorphisms UniMath.AlgebraicTheories.IndexedSetCategory UniMath.AlgebraicTheories.PresheafCategoryCore UniMath.AlgebraicTheories.PresheafMorphisms UniMath.AlgebraicTheories.Presheaves