Definition pb_psfunctor_data : psfunctor_data (slice_bicat b₂) (slice_bicat b₁). Proof. use make_psfunctor_data. - exact (λ g, pb_obj f (pr2 g) ,, pb_pr1 f (pr2 g)). - simple refine (λ g₁ g₂ α, _ ,, _). + exact (f /≃₁ pr2 α). + exact (inv_of_invertible_2cell (pb_on_1cell_pr1 f (pr2 α))). - intros g₁ g₂ α β p. simple refine (_ ,, _). + exact (f /≃₂ pr2 p). + exact (pb_on_2cell_coh (pr2 α) (pr2 β) (pr1 p) (pr2 p)). - intro g. simple refine (_ ,, _). + exact (pb_1cell_on_id f (pr2 g)). + exact (pb_1cell_on_id_coh f (pr2 g)). - intros g₁ g₂ g₃ α β ; cbn. simple refine (_ ,, _). + exact (pb_1cell_on_comp f (pr2 α) (pr2 β)). + exact (pb_1cell_on_comp_coh f (pr2 α) (pr2 β)). 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.