proposition: Lemma pr1_transportf_mor_disp_reindexing_forward {a' b' : C'} {f' g' : a' --> b'} {x' :ob_disp reindexing_forward_ob_mor a'} {y' :ob_disp reindexing_forward_ob_mor b'} (e : f' = g') (ff' : x' -->[f'] y') : pr1 (transportf (mor_disp x' y') e ff') = pr1 ff'.
proof: Proof. destruct e. reflexivity. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.StreetFibration