proposition: Lemma scalar_extension_preserves_monoid_monoid_action_is_inverse : is_inverse_in_precat (C := HSET) scalar_extension_preserves_monoid_monoid_action_mor scalar_extension_preserves_monoid_monoid_action_inv.
proof: Proof. split. - apply funextfun. intro x. use (issurjsetquotpr _ x (_ ,, isasetsetquot _ _ _) _). intro y. refine (!maponpaths _ (pr2 y) @ _ @ pr2 y). apply iscompsetquotpr. apply eqrel_impl. apply hinhpr. exists (pr11 y). split. + exact (!lunax _ _). + apply idpath. - apply funextfun. intro m. refine (maponpaths (λ x, x * _) (monoidfununel f) @ _). exact (lunax _ _). 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