Proposition lax_monoidal_functor_laws_to_monoidal_laws {V₁ V₂ : monoidal_cat} {F : V₁ ⟶ V₂} {μ : ∏ (x y : V₁), F x ⊗ F y --> F(x ⊗ y)} {η : I_{V₂} --> F(I_{V₁})} (HF : lax_monoidal_functor_laws F μ η) : fmonoidal_laxlaws (μ,, η). Proof. repeat split. - intros x y₁ y₂ g ; cbn. refine (_ @ pr1 HF _ _ _ _ (identity _) g @ _). + apply maponpaths_2. unfold monoidal_cat_tensor_mor, functoronmorphisms1. refine (!(id_left _) @ _). apply maponpaths_2. rewrite functor_id. refine (!_). apply (bifunctor_rightid (pr2 V₂)). + do 2 apply maponpaths. unfold monoidal_cat_tensor_mor, functoronmorphisms1. refine (_ @ id_left _). apply maponpaths_2. apply (bifunctor_rightid (pr2 V₁)). - intros x₁ x₂ y f ; cbn. refine (_ @ pr1 HF _ _ _ _ f (identity _) @ _). + apply maponpaths_2. unfold monoidal_cat_tensor_mor, functoronmorphisms1. refine (!(id_right _) @ _). apply maponpaths. rewrite functor_id. refine (!_). apply (bifunctor_leftid (pr2 V₂)). + do 2 apply maponpaths. unfold monoidal_cat_tensor_mor, functoronmorphisms1. refine (_ @ id_right _). apply maponpaths. apply (bifunctor_leftid (pr2 V₁)). - intros x y z ; cbn. refine (_ @ pr222 HF x y z @ _). + do 2 apply maponpaths_2. unfold monoidal_cat_tensor_mor, functoronmorphisms1. refine (!(id_right _) @ _). apply maponpaths. refine (!_). apply (bifunctor_leftid (pr2 V₂)). + apply maponpaths_2. apply maponpaths. unfold monoidal_cat_tensor_mor, functoronmorphisms1. refine (_ @ id_left _). apply maponpaths_2. apply (bifunctor_rightid (pr2 V₂)). - intros x ; cbn. refine (_ @ pr12 HF x). do 2 apply maponpaths_2. unfold monoidal_cat_tensor_mor, functoronmorphisms1. refine (!(id_right _) @ _). apply maponpaths. refine (!_). apply (bifunctor_leftid (pr2 V₂)). - intros x ; cbn. refine (_ @ pr122 HF x). do 2 apply maponpaths_2. unfold monoidal_cat_tensor_mor, functoronmorphisms1. refine (!(id_left _) @ _). apply maponpaths_2. refine (!_). apply (bifunctor_rightid (pr2 V₂)). Qed.
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.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Import BifunctorNotations. Import MonoidalNotations.