proposition: Lemma fiber_limit_arrow_commutes : is_cone_mor d'_cone (fiber_lim_out,, fiber_lim_out_commutes) fiber_limit_arrow.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions