Definition creates_limit {C : category} {D : disp_cat C} {J : graph} (F : diagram J (total_category D)) (L : LimCone (mapdiagram (pr1_category D) F)) : UU := ∑ (CC : ( ∑ (d : D (lim L)) (δ : ∏ j : vertex J, d -->[limOut L j] (pr2 (dob F j))), forms_cone (c := (lim L ,, d)) F (λ j, (limOut L j ,, δ j)))) , isLimCone _ _ (make_cone _ (pr2 (pr2 CC))).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.