Definition endomorphism_monoid {C : category} (X : ob C) : monoid. Proof. use make_monoid. - use make_setwithbinop. + use make_hSet. * exact (X --> X). * apply homset_property. + exact (@compose C X X X). - use make_dirprod. + exact (fun x x' x'' => !(@assoc C _ _ _ _ x x' x'')). + refine (identity X,, _). split. * exact (@id_left C X X). * exact (@id_right C X X). Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.Additive. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.Categories.HSET.Core.