Definition creates_limits_sigma_disp_cat {J : graph} (F : diagram J (total_category sigma_disp_cat)) (L : LimCone (mapdiagram (pr1_category _) F)) (HD : creates_limit (mapdiagram (total_functor sigmapr1_disp_functor) F) L) (HE : creates_limit (mapdiagram sigma_to_E_total_functor F) (total_limit _ HD)) : creates_limit F L := make_creates_limit (tip_sigma_disp_cat HD HE) (cone_sigma_disp_cat HD HE) (forms_cone_sigma_disp_cat HD HE) (is_lim_cone_sigma_disp_cat HD HE).
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.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Adjunctions.Core. 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.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Limits.