Lemma mfbracket_natural {Z Z' : PtdV} (f : Z --> Z') (g : pr1 Z' --> gh) : pr1 f ⊗^{ Mon_V}_{r} gh · ⦃g⦄_{Z'} = ⦃pr1 f · g⦄_{Z}. Proof. apply mfbracket_unique. split. - etrans. 2: { rewrite assoc. apply cancel_postcomposition. apply (bifunctor_equalwhiskers Mon_V). } unfold functoronmorphisms1. etrans. 2: { rewrite assoc'. apply maponpaths. apply mfbracket_η. } repeat rewrite assoc. apply cancel_postcomposition. apply pathsinv0, monoidal_rightunitornat. - etrans. 2: { rewrite assoc. apply cancel_postcomposition. apply (bifunctor_equalwhiskers Mon_V). } unfold functoronmorphisms1. etrans. 2: { rewrite assoc'. apply maponpaths. apply mfbracket_τ. } rewrite functor_comp. repeat rewrite assoc. do 2 apply cancel_postcomposition. apply pathsinv0, (lineator_linnatright Mon_PtdV Act Act). 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.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids. Require Import UniMath.CategoryTheory.Actegories.Actegories. Require Import UniMath.CategoryTheory.Actegories.ConstructionOfActegories. Require Import UniMath.CategoryTheory.Actegories.MorphismsOfActegories. Require Import UniMath.CategoryTheory.Actegories.CoproductsInActegories. Require Import UniMath.CategoryTheory.coslicecat. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects. Import BifunctorNotations. Import MonoidalNotations.