proposition: Lemma actorinv_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'⟧) : (f ⊗^{Act} (g ⊗^{Act} h)) · (aαinv_{Act} v' w' z') = (aαinv_{Act} v w z) · ((f ⊗^{Mon_V} g) ⊗^{Act} h).
proof: Proof. intros. unfold functoronmorphisms1. apply actorinv_nat1. 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