proposition: Lemma pr22_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') : pr22 (transportf (mor_disp x' y') e ff') = transportf (mor_disp (pr22 x') (pr22 y')) (! pr1_transportf_mor_disp_reindexing_forward e ff') (pr22 ff').
proof: Proof. destruct e. reflexivity. Qed.
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