proposition: Lemma pentagon_identity_actorinv {C : category} (Act : actegory C) (w v u : V) (z : C): w ⊗^{ Act}_{l} (aαinv_{Act} v u z) · aαinv_{Act} w (v ⊗_{Mon_V} u) z · αinv_{Mon_V} w v u ⊗^{Act}_{r} z = aαinv_{Act} w v (u ⊗_{Act} z) · aαinv_{Act} (w ⊗_{Mon_V} v) u z.
proof: Proof. apply pathsinv0. apply (z_iso_inv_on_right _ _ _ (z_iso_from_actor_iso Act _ _ _)). unfold z_iso_from_actor_iso. unfold make_z_iso. unfold make_is_z_isomorphism. etrans. { apply (pathsinv0 (id_right _)). } apply (z_iso_inv_on_right _ _ _ (z_iso_from_actor_iso Act _ _ _)). cbn. apply pathsinv0. etrans. { rewrite assoc. apply cancel_postcomposition. apply (pathsinv0 (actegory_pentagonidentity Act w v u z)). } etrans. { rewrite assoc. rewrite assoc. apply cancel_postcomposition. apply cancel_postcomposition. rewrite assoc'. apply cancel_precomposition. apply (pathsinv0 (bifunctor_leftcomp Act _ _ _ _ _ _)). } etrans. { apply cancel_postcomposition. apply cancel_postcomposition. apply cancel_precomposition. apply maponpaths. apply (pr2 (z_iso_from_actor_iso Act v u z)). } etrans. { apply cancel_postcomposition. apply cancel_postcomposition. apply cancel_precomposition. apply (bifunctor_leftid Act). } etrans. { apply cancel_postcomposition. apply cancel_postcomposition. apply id_right. } etrans. { apply cancel_postcomposition. rewrite assoc'. apply cancel_precomposition. apply (pr2 (z_iso_from_actor_iso Act w (v⊗_{Mon_V}u) z)). } etrans. { apply cancel_postcomposition. apply id_right. } etrans. { apply (pathsinv0 (bifunctor_rightcomp Act _ _ _ _ _ _)). } etrans. { apply maponpaths. apply (pr2 (pr2 (z_iso_from_associator_iso Mon_V w v u))). } apply (bifunctor_rightid Act). 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