Definition creates_limit_unique_disp_struct {C : category} {P H Hprop Hid Hcomp} (D := disp_struct C P H Hprop Hid Hcomp) {J : graph} {F : diagram J (total_category D)} {L : LimCone (mapdiagram (pr1_category D) F)} (CC : creates_limit F L) (d_is_unique : ∏ d', (∏ j : vertex J, d' -->[limOut L j] (pr2 (dob F j))) → d' = pr11 CC) : creates_limit_unique F L. Proof. use (make_creates_limit_unique CC). abstract ( intros d δ H0; apply subtypePairEquality; [ intro; use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)); repeat (apply impred_isaprop; intro); [ apply Hprop | apply (homset_property (total_category _)) ] | exact (d_is_unique _ δ) ] ). 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.