Definition reindexing_forward_ob_mor : disp_cat_ob_mor C'. Proof. use make_disp_cat_ob_mor. - exact (λ c', ∑c:C,(F c=c' × ob_disp D c)). - intros a' b' x' y' f'. exact (∑f:(↙ x')-->(↙ y'), (double_transport (¤ x') (¤ y') (# F f)=f' × (← x')-->[f](← y'))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.StreetFibration.