Definition act_pentagon : action_pentagon_eq act_odot act_χ := pr2 (pr2 (pr2 (pr2 actn))). End Projections. Section Alternative_Definition. Let Mon_EndA : monoidal_cat := monoidal_cat_of_endofunctors A. Context (FF: strong_monoidal_functor Mon_V Mon_EndA). Let ϵ : functor_identity A ⟹ (FF I: functor A A) := lax_monoidal_functor_ϵ FF. Let ϵ_inv : (FF I: functor A A) ⟹ functor_identity A := strong_monoidal_functor_ϵ_inv FF. Let μ : monoidal_functor_map Mon_V Mon_EndA FF := lax_monoidal_functor_μ FF. Let ϵ_is_z_iso : is_z_isomorphism (lax_monoidal_functor_ϵ FF) := strong_monoidal_functor_ϵ_is_z_iso FF. Let μ_is_nat_z_iso : is_nat_z_iso (lax_monoidal_functor_μ FF) := strong_monoidal_functor_μ_is_nat_z_iso FF. Let FFunital : monoidal_functor_unitality Mon_V Mon_EndA FF (lax_monoidal_functor_ϵ FF) (lax_monoidal_functor_μ FF) := lax_monoidal_functor_unital FF. Let FFassoc : monoidal_functor_associativity Mon_V Mon_EndA FF (lax_monoidal_functor_μ FF) := lax_monoidal_functor_assoc FF. Local Definition odot : functor (category_binproduct A Mon_V) A := uncurry_functor _ _ _ FF. Local Definition auxρ : nat_z_iso (odot_I_functor odot) (FF I: functor A A). Proof. use make_nat_z_iso. - use tpair. + intro F. apply identity. + cbn. intros F F' α. unfold functor_fix_snd_arg_data. cbn. rewrite id_left, id_right. assert (H := functor_id FF I). apply (maponpaths (fun f => pr1 f F')) in H. etrans. { apply maponpaths. exact H. } apply id_right. - intro F. use make_is_z_isomorphism. + apply identity. + split; apply id_left. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored. Require Import UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal.