Definition creates_limit_unique_disp_full_sub {C : category} {P : C → UU} (D := disp_full_sub C P) (H : ∏ c, isaprop (P c)) {J : graph} {F : diagram J (total_category D)} (L : LimCone (mapdiagram (pr1_category D) F)) (CC : creates_limit F L) : creates_limit_unique F L. Proof. use (make_creates_limit_unique CC). abstract ( do 3 intro; apply subtypePairEquality'; [ apply H | use (isaprop_total2 (_ ,, _) (λ _, _ ,, _)); [ apply impred_isaprop; intro; apply isapropunit | do 3 (apply impred_isaprop; intro); simpl; apply isaset_dirprod; [ apply homset_property | apply isasetunit] ] ] ). 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.