proposition: Lemma scalar_extension_preserves_monoid_monoid_action_mor_iscomprelfun : iscomprelfun (eqrelation _) scalar_extension_preserves_monoid_monoid_action_mor_fun.
proof: Proof. intros x x' Hx. use (Hx (make_eqrel (λ x x', make_hProp _ _) _) _). - apply setproperty. - repeat split. + intros y y' y'' Hy Hy'. now rewrite Hy, Hy'. + now intros y y' Hy. - intros y y' Hy. use Hy. intro H. refine (maponpaths _ (pr22 H) @ !_). refine (maponpaths (λ x, _ x * _) (pr12 H) @ _). refine (maponpaths (λ x, x * _) (monoidfunmul f _ _) @ _). apply assocax. 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