Proposition is_mon_nat_trans_prewhisker {C₁ C₂ C₃ : category} {M₁ : monoidal C₁} {M₂ : monoidal C₂} {M₃ : monoidal C₃} {F : C₁ ⟶ C₂} (HF : fmonoidal_lax M₁ M₂ F) {G₁ G₂ : C₂ ⟶ C₃} {HG₁ : fmonoidal_lax M₂ M₃ G₁} {HG₂ : fmonoidal_lax M₂ M₃ G₂} {τ : G₁ ⟹ G₂} (Hτ : is_mon_nat_trans HG₁ HG₂ τ) : is_mon_nat_trans (comp_fmonoidal_lax HF HG₁) (comp_fmonoidal_lax HF HG₂) (pre_whisker F τ). Proof. split. - intros x y ; cbn. unfold fmonoidal_preservestensordata. assert (aux := pr1 Hτ (F x) (F y)). unfold fmonoidal_preservestensordata in aux. etrans. 2: { rewrite assoc. apply cancel_postcomposition. exact aux. } clear aux. repeat rewrite assoc'. apply maponpaths. apply nat_trans_ax. - unfold is_mon_nat_trans_unitlaw ; cbn. unfold fmonoidal_preservesunit. assert (aux := pr2 Hτ). red in aux. unfold fmonoidal_preservesunit in aux. rewrite <- aux. repeat rewrite assoc'. apply maponpaths. apply nat_trans_ax. 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.