proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Symmetric