Definition creates_limit_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)) (d : D (lim L)) (cone : ∏ j : vertex J, d -->[limOut L j] (pr2 (dob F j))) (is_limit : ∏ (d' : total_category D) (cone_out : ∏ u, d' --> (dob F u)) (is_cone : ∏ u v e, cone_out u · (dmor F e) = cone_out v) (L_lim_arrow := limArrow L _ (make_cone (d := (mapdiagram (pr1_category D) F)) _ (λ u v e, maponpaths pr1 (is_cone u v e)))), pr2 d' -->[L_lim_arrow] d) : creates_limit F L. Proof. use (make_creates_limit d cone _ (λ d' cone', (_ ,, _) ,, _)). - abstract ( do 3 intro; apply (subtypePairEquality (λ _, Hprop _ _ _ _ _)); apply (limOutCommutes L) ). - exact (_ ,, is_limit d' (pr1 cone') (pr2 cone')). - abstract ( intro u; apply (subtypePairEquality (λ _, Hprop _ _ _ _ _)); exact (limArrowCommutes L _ _ _) ). - abstract ( intro t; repeat apply subtypePairEquality; [ intro; apply impred_isaprop; intro; apply (homset_property (total_category _)) | simpl; intro; apply Hprop | apply (limArrowUnique L); intro; exact (maponpaths pr1 (pr2 t u)) ] ). 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.