proposition: Lemma compute_mfbracket {Z : PtdV} (f : Z --> Ptd_from_mhss) : ⦃pr1 f⦄_{Z} = pr1 f ⊗^{ Mon_V}_{r} gh · ⦃identity gh⦄_{Ptd_from_mhss}.
proof: Proof. etrans. { rewrite <- (id_right (pr1 f)). apply pathsinv0, mfbracket_natural. } apply idpath. 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.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids UniMath.CategoryTheory.Actegories.Actegories UniMath.CategoryTheory.Actegories.ConstructionOfActegories UniMath.CategoryTheory.Actegories.MorphismsOfActegories UniMath.CategoryTheory.Actegories.CoproductsInActegories UniMath.CategoryTheory.coslicecat UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects