proposition: Lemma coprod_antidistributor_pentagon_identity (v w : V) (cs : power_category I C) : # (coproduct_functor I CP) aα^{actegory_power Mon_V I Act}_{v, w, cs} · actegory_coprod_antidistributor v (fun i => w ⊗_{Act} (cs i)) · v ⊗^{Act}_{l} actegory_coprod_antidistributor w cs = actegory_coprod_antidistributor (v ⊗_{Mon_V} w) cs · aα^{Act}_{v, w, coproduct_functor I CP cs}.
proof: Proof. etrans. { rewrite assoc'. apply postcompWithCoproductArrow. } etrans. 2: { apply pathsinv0, postcompWithCoproductArrow. } apply maponpaths; apply funextsec; intro i. etrans. { repeat rewrite assoc. apply cancel_postcomposition. rewrite assoc'. apply maponpaths. apply CoproductInCommutes. } etrans. 2: { apply actegory_actornatleft. } rewrite assoc'. apply maponpaths. etrans. { apply pathsinv0, (functor_comp (leftwhiskering_functor Act v)). } apply maponpaths. apply CoproductInCommutes. 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.Functors UniMath.CategoryTheory.Actegories.Actegories UniMath.CategoryTheory.Actegories.MorphismsOfActegories UniMath.CategoryTheory.Actegories.ProductActegory UniMath.CategoryTheory.Actegories.ConstructionOfActegories UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.ProductCategory UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts