proposition: Lemma mbracket_property_single_equivalent {z : V} (e : I_{Mon_V} --> z) (f : z --> t) (h : z ⊗_{Mon_V} t --> t) : mbracket_property_parts e f h <-> mbracket_property_single e f h.
proof: Proof. split. - intros [Hη Hτ]. use BinCoproductArrowsEq. + etrans. { repeat rewrite assoc. do 2 apply cancel_postcomposition. apply BinCoproductIn1Commutes. } etrans. { apply cancel_postcomposition. apply pathsinv0, (functor_comp (leftwhiskering_functor Act (z,,e))). } rewrite BinCoproductIn1Commutes. etrans. 2: { repeat rewrite assoc. do 2 apply cancel_postcomposition. apply pathsinv0, BinCoproductOfArrowsIn1. } etrans. { apply pathsinv0, Hη. } repeat rewrite assoc'. apply maponpaths. rewrite assoc. etrans. 2: { apply cancel_postcomposition. apply pathsinv0, BinCoproductOfArrowsIn1. } rewrite assoc'. rewrite id_left. apply pathsinv0, BinCoproductIn1Commutes. + etrans. { repeat rewrite assoc. do 2 apply cancel_postcomposition. apply BinCoproductIn2Commutes. } etrans. { apply cancel_postcomposition. apply pathsinv0, (functor_comp (leftwhiskering_functor Act (z,,e))). } rewrite BinCoproductIn2Commutes. etrans. 2: { repeat rewrite assoc. do 2 apply cancel_postcomposition. apply pathsinv0, BinCoproductOfArrowsIn2. } etrans. { apply pathsinv0, Hτ. } repeat rewrite assoc'. apply maponpaths. rewrite assoc. etrans. 2: { apply cancel_postcomposition. apply pathsinv0, BinCoproductOfArrowsIn2. } rewrite assoc'. apply maponpaths. apply pathsinv0, BinCoproductIn2Commutes. - intro H1. split. + apply (maponpaths (fun m => BinCoproductIn1 (CP _ _) · m)) in H1. unfold actegory_bincoprod_antidistributor, bifunctor_bincoprod_antidistributor, bincoprod_antidistributor in H1. repeat rewrite assoc in H1. rewrite BinCoproductIn1Commutes in H1. assert (aux := functor_comp (leftwhiskering_functor Act (z,,e)) (BinCoproductIn1 (CP I_{ Mon_V} (H t))) (BinCoproductArrow (CP I_{ Mon_V} (H t)) η τ)). cbn in aux. apply (maponpaths (fun m => m · h)) in aux. assert (H1' := aux @ H1). clear H1 aux. rewrite BinCoproductIn1Commutes in H1'. etrans. 2: { apply pathsinv0, H1'. } clear H1'. etrans. 2: { repeat rewrite assoc. do 2 apply cancel_postcomposition. apply pathsinv0, BinCoproductOfArrowsIn1. } repeat rewrite assoc'. apply maponpaths. rewrite assoc. etrans. 2: { apply cancel_postcomposition. apply pathsinv0, BinCoproductOfArrowsIn1. } rewrite assoc'. rewrite id_left. apply pathsinv0, BinCoproductIn1Commutes. + apply (maponpaths (fun m => BinCoproductIn2 (CP _ _) · m)) in H1. unfold actegory_bincoprod_antidistributor, bifunctor_bincoprod_antidistributor, bincoprod_antidistributor in H1. repeat rewrite assoc in H1. rewrite BinCoproductIn2Commutes in H1. assert (aux := functor_comp (leftwhiskering_functor Act (z,,e)) (BinCoproductIn2 (CP I_{ Mon_V} (H t))) (BinCoproductArrow (CP I_{ Mon_V} (H t)) η τ)). cbn in aux. apply (maponpaths (fun m => m · h)) in aux. assert (H1' := aux @ H1). clear H1 aux. rewrite BinCoproductIn2Commutes in H1'. etrans. 2: { apply pathsinv0, H1'. } clear H1'. etrans. 2: { repeat rewrite assoc. do 2 apply cancel_postcomposition. apply pathsinv0, BinCoproductOfArrowsIn2. } repeat rewrite assoc'. apply maponpaths. rewrite assoc. etrans. 2: { apply cancel_postcomposition. apply pathsinv0, BinCoproductOfArrowsIn2. } rewrite assoc'. apply maponpaths. apply pathsinv0, BinCoproductIn2Commutes. 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