Definition reindex_pb_ump_1_data : functor_data C₀ (total_category (reindex_disp_cat F D₂)). Proof. use make_functor_data. - exact (λ x, H x ,, pr1 (HD₂ _ _ (nat_z_iso_pointwise_z_iso α x) (pr2 (G x)))). - refine (λ x y f, # H f ,, _). refine (transportb (λ z, _ -->[ z ] _) _ (pr2 (HD₂ _ _ (nat_z_iso_pointwise_z_iso α x) (pr2 (G x))) ;; (pr2 (#G f))%cat ;; inv_mor_disp_from_z_iso (pr2 (HD₂ _ _ (nat_z_iso_pointwise_z_iso α y) (pr2 (G y)))))%mor_disp). abstract (cbn ; use z_iso_inv_on_left ; refine (!_) ; exact (nat_trans_ax α _ _ f)). Defined.
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.