Definition make_creates_limit_unique {C : category} {D : disp_cat C} {J : graph} {F : diagram J (total_category D)} {L : LimCone (mapdiagram (pr1_category D) F)} (CC : creates_limit F L) (Hunique : ∏ (d : D (lim L)) (δ : ∏ j : vertex J, d -->[limOut L j] (pr2 (dob F j))) (H : forms_cone (c := (lim L ,, d)) F (λ j, (limOut L j ,, δ j))), (d ,, δ ,, H) = pr1 CC ) : creates_limit_unique F L. Proof. refine ((pr1 CC ,, _) ,, pr2 CC). exact (λ _, Hunique _ _ _). Defined.
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.