proposition: Lemma actegory_unitorinvnat {C : category} (Act : actegory C) : action_unitorinv_nat auinv_{Act}.
proof: Proof. intros x y f. apply (z_iso_inv_on_right _ _ _ (_,,_,,actegory_unitorisolaw Act x)). cbn. rewrite assoc. apply (z_iso_inv_on_left _ _ _ _ (_,,_,,actegory_unitorisolaw Act y)). apply pathsinv0, actegory_unitornat. 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