proposition: Lemma fiber_lim_out_commutes (u v : vertex J) (e : edge u v) : transportf _ (id_right _) (fiber_lim_out u ;; dmor F e) = fiber_lim_out v.
proof: Proof. unfold fiber_lim_out. rewrite mor_disp_transportf_postwhisker. apply transportf_transpose_right. refine (_ @ maponpaths _ (fiber_paths (pr221 H u v e))). rewrite mor_disp_transportf_prewhisker. simpl. rewrite assoc_disp. apply transportf_transpose_right. apply transportf_transpose_right. 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