proposition: Lemma bincoprod_antidistributor_pentagon_identity (v w : V) (cd : category_binproduct C C) : # (bincoproduct_functor BCP) aα^{actegory_binprod Mon_V Act Act}_{v, w, cd} · actegory_bincoprod_antidistributor v (w ⊗_{Act} pr1 cd) (w ⊗_{ Act} pr2 cd) · v ⊗^{Act}_{l} actegory_bincoprod_antidistributor w (pr1 cd) (pr2 cd) = actegory_bincoprod_antidistributor (v ⊗_{Mon_V} w) (pr1 cd) (pr2 cd) · aα^{Act}_{v, w, bincoproduct_functor BCP cd}.
proof: Proof. etrans. { rewrite assoc'. apply postcompWithBinCoproductArrow. } etrans. 2: { apply pathsinv0, postcompWithBinCoproductArrow. } apply maponpaths_12. - etrans. { repeat rewrite assoc. apply cancel_postcomposition. rewrite assoc'. apply maponpaths. apply BinCoproductIn1Commutes. } etrans. 2: { apply actegory_actornatleft. } rewrite assoc'. apply maponpaths. etrans. { apply pathsinv0, (functor_comp (leftwhiskering_functor Act v)). } apply maponpaths. apply BinCoproductIn1Commutes. - etrans. { repeat rewrite assoc. apply cancel_postcomposition. rewrite assoc'. apply maponpaths. apply BinCoproductIn2Commutes. } etrans. 2: { apply actegory_actornatleft. } rewrite assoc'. apply maponpaths. etrans. { apply pathsinv0, (functor_comp (leftwhiskering_functor Act v)). } apply maponpaths. apply 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.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