proposition: Lemma actor_nat2 {C : category} (Act : actegory C) {v v' w w' : V} {z z' : C} (f : V⟦v,v'⟧) (g : V⟦w,w'⟧) (h : C⟦z,z'⟧) : (actegory_actordata Act v w z) · (f ⊗^{Act} (g ⊗^{Act} h)) = ((f ⊗^{Mon_V} g) ⊗^{Act} h) · (actegory_actordata Act v' w' z').
proof: Proof. intros. unfold functoronmorphisms1. exact (actor_nat1 Act f g h). Qed.
imports: UniMath.MoreFoundations.All UniMath.Foundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Equivalences.FullyFaithful UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories