proposition: Lemma monoid_action_cat_induced_morphism_commutes : F = #(constprod_functor1 (binproducts_monoid_action_cat M) X) monoid_action_cat_induced_morphism · exponential_object_morphism.
proof: Proof. apply monoid_action_morphism_eq. intro x. cbn. apply (maponpaths (λ y, F (_ ,, y))). exact (!action_unel _ (pr2 x)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.MonoEpiIso UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total