Definition creates_limit_unique {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 (pr1 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.