Definition reindexing_forward_id_comp : disp_cat_id_comp C' reindexing_forward_ob_mor. Proof. use tpair. - intros c' x'. exists (identity (↙ x')). use tpair. * apply (! reindexing_forward_id). * exact (id_disp (← x')). - intros a' b' c' f' g' x' y' z'. intros Df' Dg'. exists ((↙ Df')·(↙ Dg')). use tpair. * apply (! reindexing_forward_comp). * exact (comp_disp (← Df') (← Dg')). 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.