Monoid instance on End(X)

Stream: Is there code for X?

[Adam Topaz]

If $\mathscr{C}$ is any category, and $X$ is an object of $\mathscr{C}$, then $\operatorname{Hom}(X,X)$ has an obvious monoid structure. Does this exist in mathlib?
apply_instance comes up empty here:

import algebra
import category_theory.category

open category_theory

variables {C : Type*} [category C]
variables {X : C}

example : monoid (X ⟶ X) := by apply_instance

If it's not already in mathlib, does it make sense to introduce such an instance?

[Bhavik Mehta]

Look in ct.endomorphism

[Adam Topaz]

Thanks!