Lemma actegory_laws_from_object : actegory_laws (monoidal_swapped Mon_V) actegory_data_from_object. Proof. split5. - apply bifunctor_data_from_functorintoendofunctorcat_is_bifunctor. - repeat split. + intro ; intros. apply (pr212 action_fmon_strong). + apply (eqtohomot (base_paths _ _ (pr222 action_fmon_strong))). + apply (eqtohomot (base_paths _ _ (pr122 action_fmon_strong))). - repeat split. + intro ; intros. exact (! pr21 (pr1 action_fmon_strong w v) z z' h). + intros v1 v2 w c f. set (fmon_strong_preserves_tensor_inv := preservestensor_inv_is_nattrans (pr12 action_fmon_lax) (pr122 action_fmon_lax) (pr1 action_fmon_strong)). exact (! (eqtohomot (base_paths _ _ (pr12 fmon_strong_preserves_tensor_inv w _ _ f)) c)). + intros w v1 v2 c f. exact (eqtohomot (base_paths _ _ (preserves_tensorinv_nat_right (pr1 action_fmon_strong) (pr122 action_fmon_lax) v1 v2 w f)) c). + apply (eqtohomot (base_paths _ _ (pr22 (pr1 action_fmon_strong w v)))). + apply (eqtohomot (base_paths _ _ (pr12 (pr1 action_fmon_strong w v)))). - intros v c. cbn. assert (plu := preserves_leftunitality'' (_,,pr222 C) v). assert (pluc := eqtohomot (base_paths _ _ plu) c). refine (_ @ pluc). clear pluc ; clear plu. cbn. rewrite ! id_right. apply idpath. - intro ; intros. cbn. unfold actor_from_object. assert (t := ! eqtohomot (base_paths _ _ (preserves_associativity_of_inverse_preserves_tensor (pr1 (pr222 action_fmon_lax)) (pr1 action_fmon_strong) v' v w)) z). cbn in t. rewrite id_right in t. set (αisov'vw := z_iso_inv (z_iso_from_associator_iso Mon_V v' v w)). rewrite assoc' in t. assert (pf: (pr1 (is_z_isomorphism_mor (pr1 action_fmon_strong v' (v ⊗_{ Mon_V} w))) z · pr1 (is_z_isomorphism_mor (pr1 action_fmon_strong v w)) (pr1 ((pr12 C) v') z)) = pr1 (# (pr12 C) (monoidal_associatorinvdata Mon_V v' v w)) z · (pr1 (is_z_isomorphism_mor (pr1 action_fmon_strong (v' ⊗_{ Mon_V} v) w)) z · # (pr1 ((pr12 C) w)) (pr1 (is_z_isomorphism_mor (pr1 action_fmon_strong v' v)) z))). { etrans. 2: { apply maponpaths. exact t. } rewrite ! assoc. apply maponpaths_2. etrans. 2: { apply maponpaths_2. assert (bla := eqtohomot (base_paths _ _ (maponpaths (# (pr12 C)) (pr2 (monoidal_associatorisolaw Mon_V v' v w)))) z). rewrite functor_comp in bla. exact (! bla). } rewrite functor_id. apply (! id_left _). } refine (_ @ ! pf). apply assoc'. 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.