Definition transportf_reindex {C' C : category} {D : disp_cat C} {F : C' ⟶ C} {x y : C'} {xx : D(F x)} {yy : D(F y)} {f g : x --> y} (p : f = g) (ff : xx -->[# F f] yy) : transportf (@mor_disp C' (reindex_disp_cat F D) _ _ xx yy) p ff = transportf (@mor_disp C D _ _ xx yy) (maponpaths (# F) p) ff.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Section IsCartesianFromReindexDispCat. End IsCartesianFromReindexDispCat. Section IsOpCartesianFromReindexDispCat. End IsOpCartesianFromReindexDispCat.