proposition: Lemma U_action_plaw : action_pentagon_eq Mon_A otimes_U_functor U_action_χ.
proof: 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 (# tensor_A ((α_A ((a, U x), U y) #, id U z) · (# tensor_A (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 α_A ((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: Mon_A ⟦(U x ⊗_A U y) ⊗_A U z, U (x ⊗ (y ⊗ z))⟧ => id a #⊗_A u)). apply (lax_monoidal_functor_assoc U). } fold α_A. fold tensor_A. fold tensor. etrans. { rewrite assoc. apply maponpaths. rewrite assoc'. rewrite <- (id_left (id a)). intermediate_path (# tensor_A ((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 (# tensor_A ((id a #, # tensor_A (id 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 pentagon_eq_A. } repeat rewrite assoc'. apply maponpaths. etrans. { apply pathsinv0. apply (nat_trans_ax α_A ((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. unfold make_dirprod. apply cancel_postcomposition. change (# tensor_A (# tensor_A (id (a, U x)) #, lax_monoidal_functor_μ U (y, z)) = # tensor_A (id (a ⊗_A U x) #, lax_monoidal_functor_μ U (y, z))). rewrite functor_id. apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal