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. 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.
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.Functors. Require Import UniMath.CategoryTheory.Actegories.Actegories. Require Import UniMath.CategoryTheory.Actegories.MorphismsOfActegories. Require Import UniMath.CategoryTheory.Actegories.ProductActegory. Require Import UniMath.CategoryTheory.Actegories.ConstructionOfActegories. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Import BifunctorNotations. Import MonoidalNotations. Import ActegoryNotations.