proposition: Lemma monoid_action_morphism_eq {M : monoid} {X X' : monoid_action M} (f f' : monoid_action_morphism X X') (H : ∏ x, f x = f' x) : f = f'.
proof: Proof. apply subtypePath. { intro. apply isapropunit. } apply subtypePath. { intro. apply isaprop_is_monoid_action_morphism. } apply funextfun. exact H. 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