proposition: Proposition transportf_indexed_cat_to_disp_cat {x y : C} {xx : indexed_cat_to_disp_cat_data x} {yy : indexed_cat_to_disp_cat_data y} {f g : x --> y} (p : f = g) (ff : xx --> (Φ $ f) yy) : transportf (λ z, xx -->[ z ] yy) p ff = ff · idtoiso (maponpaths (λ h, (Φ $ h) yy) p).
proof: Proof. induction p ; cbn. rewrite id_right. apply idpath. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.OppositeCategory.Core UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.IndexedCategories.IndexedCategory