Definition prod_disp_psfunctor {B₁ B₂ : bicat} {D₁ D₃ : disp_bicat B₁} {D₂ D₄ : disp_bicat B₂} (HD₂ : disp_2cells_isaprop D₂) (HD₂' : disp_locally_groupoid D₂) (HD₄ : disp_2cells_isaprop D₄) (HD₄' : disp_locally_groupoid D₄) {F : psfunctor B₁ B₂} (FF₁ : disp_psfunctor D₁ D₂ F) (FF₂ : disp_psfunctor D₃ D₄ F) : disp_psfunctor (disp_dirprod_bicat D₁ D₃) (disp_dirprod_bicat D₂ D₄) F. Proof. use make_disp_psfunctor. - use disp_2cells_isaprop_prod. + exact HD₂. + exact HD₄. - use disp_locally_groupoid_prod. + exact HD₂'. + exact HD₄'. - exact (λ x xx, FF₁ x (pr1 xx) ,, FF₂ x (pr2 xx)). - exact (λ x y f xx yy ff, ♯ FF₁ (pr1 ff) ,, ♯ FF₂ (pr2 ff)). - exact (λ x y f g τ xx yy ff gg ττ, ♯♯ FF₁ (pr1 ττ) ,, ♯♯ FF₂ (pr2 ττ)). - refine (λ x xx, _ ,, _). + exact (disp_psfunctor_id _ _ _ FF₁ (pr1 xx)). + exact (disp_psfunctor_id _ _ _ FF₂ (pr2 xx)). - refine (λ x y z f g xx yy zz ff gg, _ ,, _). + exact (disp_psfunctor_comp _ _ _ FF₁ (pr1 ff) (pr1 gg)). + exact (disp_psfunctor_comp _ _ _ FF₂ (pr2 ff) (pr2 gg)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispBiequivalence. Require Import UniMath.Bicategories.DisplayedBicats.DispBuilders. Require Import UniMath.Bicategories.DisplayedBicats.DispPseudofunctor. Require Import UniMath.Bicategories.DisplayedBicats.DispTransformation. Require Import UniMath.Bicategories.DisplayedBicats.DispModification. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.PseudoFunctors.Biequivalence.