Lemma U_action_tlaw : action_triangle_eq Mon_A otimes_U_functor U_action_ρ U_action_χ. Proof. red. intros a x. cbn. unfold nat_trans_from_functor_fix_snd_morphism_arg_data. unfold nat_trans_data_post_whisker_fst_param. cbn. unfold make_dirprod. rewrite functor_id. apply pathsinv0. etrans. { rewrite assoc'. apply maponpaths. apply pathsinv0. apply functor_comp. } unfold compose at 2. simpl. unfold make_dirprod. rewrite id_left. rewrite <- (id_left (id U x)). apply pathsinv0. intermediate_path (# tensor_A ((# tensor_A (id a #, strong_monoidal_functor_ϵ_inv U)) #, id U x) · # tensor_A (ρ_A a #, id U x)). { rewrite <- functor_comp. apply idpath. } pose (f := # tensor_A (# tensor_A (id a #, lax_monoidal_functor_ϵ U) #, id U x)). apply (pre_comp_with_z_iso_is_inj'(f:=f)). { use is_z_iso_tensor_z_iso. - use is_z_iso_tensor_z_iso. + exact (identity_is_z_iso _). + exact (strong_monoidal_functor_ϵ_is_z_iso U). - exact (identity_is_z_iso _ ). } rewrite assoc. intermediate_path (# tensor_A (ρ_A a #, id U x)). { apply pathsinv0. etrans. - apply (!(id_left _)). - apply cancel_postcomposition. unfold f. rewrite <- functor_comp. apply pathsinv0. apply functor_id_id. apply pathsdirprod; simpl. + etrans. * apply pathsinv0. apply functor_comp. * apply functor_id_id. apply pathsdirprod; simpl. -- apply id_left. -- apply pathsinv0. apply z_iso_inv_on_left. rewrite id_left. apply idpath. + apply id_left. } rewrite assoc. apply pathsinv0. etrans. { apply cancel_postcomposition. apply (nat_trans_ax α_A ((a, I_A), U x) ((a, U I), U x) ((id a ,, lax_monoidal_functor_ϵ U) ,, id U x)). } simpl. etrans. { rewrite assoc'. apply maponpaths. apply pathsinv0. apply functor_comp. } unfold compose at 2. simpl. unfold make_dirprod. rewrite id_left. rewrite assoc. etrans. - apply maponpaths. eapply (maponpaths (fun u: Mon_A ⟦I_A ⊗_A (U x), U x⟧ => # tensor_A (id a #, u))). apply pathsinv0. apply (lax_monoidal_functor_unital U x). - fold λ_A. apply pathsinv0. apply triangle_eq_A. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored. Require Import UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal.