proposition: Lemma monoid_action_cat_induced_morphism_unique (t : ∑ (f' : monoid_action_morphism X'' exponential_object), F = # (constprod_functor1 (binproducts_monoid_action_cat M) X) f' · exponential_object_morphism) : t = monoid_action_cat_induced_morphism ,, monoid_action_cat_induced_morphism_commutes.
proof: Proof. use subtypePath. { intro. apply (homset_property (monoid_action_cat M)). } use monoid_action_morphism_eq. intro x''. use monoid_action_morphism_eq. intro x. refine (!_ @ maponpaths (λ x, (x : monoid_action_morphism _ _) _) (!(pr2 t))). refine (maponpaths (λ x, (_ x) _) (mor_action _ _ _) @ _). refine (maponpaths (λ x, (pr1 t x'' : monoid_action_morphism _ _) (x ,, _)) _). apply runax. 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