proposition: Lemma action_binproduct_arrow_unique (t : ∑ f, f · action_binproduct_pr1 = f1 × f · action_binproduct_pr2 = f2) : t = (_ ,, (action_binproduct_arrow_commutes1 ,, action_binproduct_arrow_commutes2)).
proof: Proof. use subtypePairEquality. { intro. use isapropdirprod; apply homset_property. } apply monoid_action_morphism_eq. intro. apply pathsdirprod. - apply (maponpaths (λ f, (f : monoid_action_morphism _ _) x) (pr12 t)). - apply (maponpaths (λ f, (f : monoid_action_morphism _ _) x) (pr22 t)). 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