proposition: Lemma reindexed_action_tlaw : action_triangle_eq Mon_V C reindexed_odot reindexed_action_right_unitor reindexed_action_convertor.
proof: Proof. red. intros a x. cbn. unfold nat_trans_from_functor_fix_snd_morphism_arg_data. unfold nat_trans_data_post_whisker_fst_param. simpl. 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 (# odotA ((# odotA (id a #, strong_monoidal_functor_ϵ_inv U)) #, id U x) · # odotA (act_ϱ actA a #, id U x)). { rewrite <- functor_comp. apply idpath. } pose (f := # odotA (# odotA (id a #, lax_monoidal_functor_ϵ U) #, id U x)). apply (pre_comp_with_z_iso_is_inj'(f:=f)). { use is_z_iso_odot_z_iso. - use is_z_iso_odot_z_iso. + exact (identity_is_z_iso _). + exact (strong_monoidal_functor_ϵ_is_z_iso U). - exact (identity_is_z_iso _ ). } rewrite assoc. intermediate_path (# odotA (act_ϱ actA 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 (act_χ actA) ((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⟧ => # odotA (id a #, u))). apply pathsinv0. apply (lax_monoidal_functor_unital U x). - fold λ_A. apply pathsinv0. apply (act_triangle actA). Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored UniMath.Bicategories.MonoidalCategories.Actions