Definition binproductleft_map_data: psfunctor_data CAT CAT. Proof. use make_psfunctor_data. - exact productwithfixedelement. - intros A A' F. exact (pair_functor F (functor_identity (pr1 B0))). - intros A A' F G α. cbn. use make_nat_trans. + intro ab. induction ab as [a b]. cbn. exact (pr1 α a ,, identity b). + intros ab ab' fg. induction ab as [a b]. induction ab' as [a' b']. induction fg as [f g]. cbn. apply pathsdirprod. * apply nat_trans_ax. * rewrite id_left. apply id_right. - intro A. cbn. use make_nat_trans. + intro ab. exact (identity ab). + intros ab ab' fg. cbn. apply pathsdirprod; rewrite id_left; apply id_right. - intros A1 A2 A3 F G. cbn. use make_nat_trans. + intro a1b. apply identity. + intros a1b a1b' fg. cbn. apply pathsdirprod; rewrite id_left; apply id_right. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfCats. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Biadjunction. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity. Require Import UniMath.Bicategories.Modifications.Modification. Import Bicat.Notations.