# Instantiating a class with a sig'd type in Coq

I can easily define a class that corresponds to the notion of a "monoidal structure" on a type M via

Definition associative {X:Type} (f : X -> X -> X) : Prop := forall x y z:X, f (f x y) z = f x (f y z).

Definition opId {X:Type} (f : X -> X -> X) (e : X) : Prop := forall x:X, f e x = x /\ f x e = x.

Class Monoid (M:Type) :=
{ binM : M -> M -> M ; idM : M ; assocMProof : associative binM ; idMProof : opId binM idM }.


and then instantiate it, for instance, with the type of endomorphisms over a given type with operation being composition:

#[refine] Instance compMon {X:Type} : Monoid (X -> X) :=
{
binM f g := fun x => f (g x) ; idM := fun x => x
}.
Proof.
- unfold associative. reflexivity.
- unfold opId. intro. split. reflexivity. reflexivity.
Defined.


but how would I, for example, go about defining the monoidal structure on the set of injective endomorphisms over a type? (Or even better, formalizing the notion that binM in compMon restricts to such a monoidal structure?) I presume I would want to define injective and then instantiate Monoid {f : X -> X | injective f} but not only would that seem to entail defining a new binary operation (which takes functions f, g and proofs of injectivity i, j and produces a new function with a new proof of injectivity) and a new identity, it seems that said binary operation wouldn't even be associative (of course $$f \circ (g \circ h) = (f \circ g) \circ h$$ as functions, but the proofs of injectivity aren't the same?). What am I missing?