Lemma reindexed_action_plaw : action_pentagon_eq Mon_V C reindexed_odot reindexed_action_convertor. Proof. red. intros a x y z. cbn. unfold nat_trans_data_post_whisker_fst_param. unfold ob1, ob2. cbn. rewrite functor_id. apply pathsinv0. etrans. { repeat rewrite assoc'. apply maponpaths. apply maponpaths. apply pathsinv0. apply functor_comp. } unfold compose at 4. cbn. unfold make_dirprod. rewrite id_left. etrans. { rewrite assoc. apply cancel_postcomposition. apply cancel_postcomposition. rewrite <- (id_left (id U z)). intermediate_path (# odotA ((act_χ actA ((a, U x), U y) #, id U z) · (# odotA (id a #, lax_monoidal_functor_μ U (x, y)) #, id U z))). - apply idpath. - apply functor_comp. } etrans. { apply cancel_postcomposition. rewrite assoc'. apply maponpaths. apply (nat_trans_ax (act_χ actA) ((a, U x ⊗_A U y), U z) ((a, U (x ⊗ y)), U z) ((id a ,, lax_monoidal_functor_μ U (x, y)) ,, id U z)). } etrans. { unfold assoc_right. cbn. rewrite assoc'. apply maponpaths. rewrite assoc'. apply maponpaths. apply pathsinv0. apply functor_comp. } unfold compose at 3. cbn. unfold make_dirprod. rewrite id_left. etrans. { do 2 apply maponpaths. rewrite assoc. eapply (maponpaths (fun u: A ⟦(U x ⊗_A U y) ⊗_A U z, U (x ⊗ (y ⊗ z))⟧ => # odotA (id a #, u))). apply (lax_monoidal_functor_assoc U). } etrans. { rewrite assoc. apply maponpaths. rewrite assoc'. rewrite <- (id_left (id a)). intermediate_path (# odotA ((id a #, α_A ((U x, U y), U z)) · (id a #, # tensor_A (id U x #, lax_monoidal_functor_μ U (y, z)) · lax_monoidal_functor_μ U (x, y ⊗ z)))). 2: { apply functor_comp. } apply idpath. } etrans. { do 2 apply maponpaths. rewrite <- (id_left (id a)). intermediate_path (# odotA ((id a #, # tensor_A (id pr1 (pr1 U) x #, lax_monoidal_functor_μ U (y, z))) · (id a #, lax_monoidal_functor_μ U (x, y ⊗ z)))). 2: { apply functor_comp. } apply idpath. } repeat rewrite assoc. apply cancel_postcomposition. etrans. { apply cancel_postcomposition. apply pathsinv0. apply (act_pentagon actA). } fold odotA. change (act_χ actA ((odotA (a, U x), U y), U z) · act_χ actA ((a, U x), tensor_A (U y, U z)) · # odotA (id a #, # tensor_A (id U x #, lax_monoidal_functor_μ U (y, z))) = act_χ actA ((odotA (a , U x), U y), U z) · # odotA (id (odotA (a , U x)) #, lax_monoidal_functor_μ U (y, z)) · act_χ actA ((a, U x), U (y ⊗ z))). repeat rewrite assoc'. apply maponpaths. etrans. { apply pathsinv0. apply (nat_trans_ax (act_χ actA) ((a, U x), U y ⊗_A U z) ((a, U x), U (y ⊗ z)) ((id a ,, id U x) ,, lax_monoidal_functor_μ U (y, z))). } cbn. apply cancel_postcomposition. change (# odotA (# odotA (id (a, U x)) #, (lax_monoidal_functor_μ U) (y, z)) = # odotA (id (odotA (a, U x)) #, lax_monoidal_functor_μ U (y, z))). rewrite functor_id. apply idpath. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.All. 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.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.Actions.