Definition creates_limit_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)) (d : P (lim L)) : creates_limit F L. Proof. use (make_creates_limit (d : (D _)) _ _ (λ d' cone', (_ ,, _) ,, _)). - abstract exact (λ _, tt). - abstract ( do 3 intro; apply subtypePairEquality'; [ apply (limOutCommutes L) | apply isapropunit ] ). - use (_ ,, tt). apply limArrow. exact (mapcone (pr1_category D) F cone'). - abstract ( intro; apply subtypePairEquality'; [ apply (limArrowCommutes L) | apply isapropunit ] ). - abstract ( intro; repeat apply subtypePairEquality'; [ apply limArrowUnique; intro; exact (maponpaths pr1 (pr2 t u)) | abstract apply isapropunit | apply impred_isaprop; intro; apply (homset_property (total_category _)) ] ). 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.