proposition: Lemma acat_to_acti_on_mor_laws {a1 a2 : ACAT} (f : ACAT⟦a1,a2⟧) : ActionBasedStrongFunctorsWhiskeredMonoidal.param_distr_bicat_triangle_eq (monoidal_swapped Mon_V) (pr22 (actegory_to_object Mon_V ax2 (pr2 a1))) (pr22 (actegory_to_object Mon_V ax2 (pr2 a2))) (pr1 f) (acat_to_acti_on_mor_data f) × ActionBasedStrongFunctorsWhiskeredMonoidal.param_distr_bicat_pentagon_eq (monoidal_swapped Mon_V) (pr22 (actegory_to_object Mon_V ax2 (pr2 a1))) (pr22 (actegory_to_object Mon_V ax2 (pr2 a2))) (pr1 f) (acat_to_acti_on_mor_data f).
proof: Proof. split. - use nat_trans_eq. { apply homset_property. } intro c ; cbn ; rewrite ! id_left ; apply actegory_hom_preserves_unitor_inv. - intros v w. use nat_trans_eq. { apply homset_property. } intro c ; cbn ; rewrite ! id_left ; assert (t := pr122 (pr22 f) w v c) ; apply (z_iso_inv_on_right _ _ _ (_,,_,,actegory_actorisolaw Mon_V (pr2 a2) _ _ _)) ; rewrite assoc ; set (i := (_,,_,,actegory_actorisolaw Mon_V (pr2 a1) w v c) : z_iso _ _) ; apply (z_iso_inv_on_left _ _ _ _ (functor_on_z_iso (pr1 f) i)) ; cbn ; rewrite assoc ; rewrite t ; apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Examples.BicatOfCats UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Actegories.Actegories UniMath.CategoryTheory.Actegories.MorphismsOfActegories UniMath.Bicategories.MonoidalCategories.BicatOfActegories UniMath.Bicategories.MonoidalCategories.BicatOfActionsInBicat UniMath.Bicategories.MonoidalCategories.WhiskeredMonoidalFromBicategory UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Biequivalence UniMath.Bicategories.Transformations.PseudoTransformation