Lemma fiber_limit_arrow_commutes : is_cone_mor d'_cone (fiber_lim_out,, fiber_lim_out_commutes) fiber_limit_arrow. Proof. unfold fiber_limit_arrow, fiber_lim_out. intro u. refine (_ @ (fiber_paths (fc u))). apply transportf_transpose_right. cbn. refine (_ @ maponpaths (λ x, x ;; (pr121 H u)) (transportb_transpose_left (pr21 g))). unfold transportb. rewrite mor_disp_transportf_postwhisker. apply transportf_transpose_right. cbn. rewrite mor_disp_transportf_prewhisker. rewrite assoc_disp. do 4 refine (transport_f_f _ _ _ _ @ _). apply transportf_set. apply homset_property. Qed.
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.