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. 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.
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.