Definition fiber_limit : LimCone F. Proof. use tpair. - use (fiber_lim ,, (fiber_lim_out ,, fiber_lim_out_commutes)). - intros d' d'_cone. exact (( _ ,, fiber_limit_arrow_commutes d' d'_cone) ,, (λ h, fiber_limit_arrow_unique d' d'_cone (pr1 h) (pr2 h)) ). 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.