Lemma actegory_hom_preserves_unitor_inv {a1 a2 : ACAT} (f : ACAT ⟦ a1, a2 ⟧) (c : pr11 (actegory_to_object Mon_V ax2 (pr2 a1))) : actegory_unitorinvdata (pr2 a2 : actegory _ _) (pr1 (pr1 f) c) · (pr12 f) I_{ Mon_V} c = # (pr11 f) (actegory_unitorinvdata (pr2 a1 : actegory _ _) c). Proof. set (t := (pr222 (pr22 f)) c). apply (z_iso_inv_on_right _ _ _ (_,,_,,actegory_unitorisolaw Mon_V (pr2 a2) (pr1 (pr1 f) c))). cbn. etrans. 2: { apply maponpaths_2 ; apply t. } rewrite assoc'. rewrite <- functor_comp. rewrite (pr1 (actegory_unitorisolaw Mon_V (pr2 a1) c)). rewrite functor_id. apply (! id_right _). 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.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.BicatOfCats. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. 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.Bicategories.MonoidalCategories.BicatOfActegories. Require Import UniMath.Bicategories.MonoidalCategories.BicatOfActionsInBicat. Require Import UniMath.Bicategories.MonoidalCategories.WhiskeredMonoidalFromBicategory. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Biequivalence. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Import BifunctorNotations. Section ActegoryFromObject. End ActegoryFromObject. Section FromActegoriesToActionsInCat. Import MonoidalNotations. End FromActegoriesToActionsInCat. Section FromActionInCatToActegories. End FromActionInCatToActegories.