Proposition is_mon_nat_trans_postwhisker {C₁ C₂ C₃ : category} {M₁ : monoidal C₁} {M₂ : monoidal C₂} {M₃ : monoidal C₃} {F₁ F₂ : C₁ ⟶ C₂} {HF₁ : fmonoidal_lax M₁ M₂ F₁} {HF₂ : fmonoidal_lax M₁ M₂ F₂} {τ : F₁ ⟹ F₂} (Hτ : is_mon_nat_trans HF₁ HF₂ τ) {G : C₂ ⟶ C₃} (HG : fmonoidal_lax M₂ M₃ G) : is_mon_nat_trans (comp_fmonoidal_lax HF₁ HG) (comp_fmonoidal_lax HF₂ HG) (post_whisker τ G). Proof. split. - intros x y ; cbn. unfold fmonoidal_preservestensordata. etrans. { rewrite assoc'. apply maponpaths. apply pathsinv0, functor_comp. } etrans. { do 2 apply maponpaths. apply (pr1 Hτ). } unfold fmonoidal_preservestensordata. rewrite functor_comp. repeat rewrite assoc. apply cancel_postcomposition. apply pathsinv0, preservestensor_is_nattrans_full. + apply (fmonoidal_preservestensornatleft HG). + apply (fmonoidal_preservestensornatright HG). - unfold is_mon_nat_trans_unitlaw ; cbn. unfold fmonoidal_preservesunit. rewrite assoc'. apply maponpaths. etrans. { apply pathsinv0, functor_comp. } apply maponpaths. apply (pr2 Hτ). 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.