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. induction p ; cbn. rewrite id_right. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.IndexedCategories.IndexedCategory.