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. 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.
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.