Definition binprod_psfunctor_data : psfunctor_data B₁ B₂. Proof. use make_psfunctor_data. - exact (λ z, F z ⊗ G z). - exact (λ x y f, #F f ⊗₁ #G f). - exact (λ x y f g α, ##F α ⊗₂ ##G α). - exact (λ b, (pair_1cell_id_id_invertible B₂ (F b) (G b))^-1 • psfunctor_id F b ⊗₂ psfunctor_id G b). - exact (λ b₁ b₂ b₃ f g, pair_1cell_comp _ (#F f) (#F g) (#G f) (#G g) • psfunctor_comp F f g ⊗₂ psfunctor_comp G f g). 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.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.Modifications.Modification. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Constant. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.Colimits.Initial. Require Import UniMath.Bicategories.Limits.Final. Require Import UniMath.Bicategories.Limits.Products. Import Products.Notations.