Definition psfunctor_binprod_ump : has_binprod_ump psfunctor_binprod_cone. Proof. use make_binprod_ump. - intro q. use make_binprod_1cell. + exact (pstrans_pair (binprod_cone_pr1 q) (binprod_cone_pr2 q)). + exact (pstrans_pair_pr1 (binprod_cone_pr1 q) (binprod_cone_pr2 q)). + exact (pstrans_pair_pr2 (binprod_cone_pr1 q) (binprod_cone_pr2 q)). - intros q α β m n. exact (prod_modification m n). - abstract (intros H α β m n ; use modification_eq ; intros x ; apply binprod_ump_2cell_pr1). - abstract (intros H α β m n ; use modification_eq ; intros x ; apply binprod_ump_2cell_pr2). - abstract (intro ; intros ; use modification_eq ; intros x ; pose (modcomponent_eq γpr1 x) as p₁ ; pose (modcomponent_eq γpr2 x) as p₂ ; pose (modcomponent_eq δpr1 x) as p₃ ; pose (modcomponent_eq δpr2 x) as p₄ ; use (binprod_ump_2cell_unique _ (pr111 α x) (pr111 β x) _ _ p₁ p₂ p₃ p₄) ; apply (pr2 B₂)). 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.