Definition disp_map_pb_psfunctor_data : psfunctor_data (disp_map_slice_bicat D b₂) (disp_map_slice_bicat D b₁). Proof. use make_psfunctor_data. - exact (λ g, pb_obj f (pr12 g) ,, pb_pr1 f (pr12 g) ,, pb_preserves_pred_ob D (pr22 g) (mirror_has_pb_ump (pb_obj_has_pb_ump f (pr12 g)))). - simple refine (λ g₁ g₂ α, _ ,, _ ,, _). + exact (f /≃₁ pr22 α). + apply pred_mor_pb_on_1cell. + exact (inv_of_invertible_2cell (pb_on_1cell_pr1 f (pr22 α))). - intros g₁ g₂ α β p. simple refine (_ ,, _). + exact (f /≃₂ pr2 p). + exact (pb_on_2cell_coh (pr22 α) (pr22 β) (pr1 p) (pr2 p)). - intro g. simple refine (_ ,, _). + exact (pb_1cell_on_id f (pr12 g)). + exact (pb_1cell_on_id_coh f (pr12 g)). - intros g₁ g₂ g₃ α β ; cbn. simple refine (_ ,, _). + exact (pb_1cell_on_comp f (pr22 α) (pr22 β)). + exact (pb_1cell_on_comp_coh f (pr22 α) (pr22 β)). 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.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.PullbackFunctions. Require Import UniMath.Bicategories.Limits.Examples.OpCellBicatLimits. Import PullbackFunctions.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Slice. Require Import UniMath.Bicategories.Logic.DisplayMapBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayMapBicatSlice.