Instantiating a class with a sig'd type in Coq

Question

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?

Answer 1

You are missing propositional extensionality. It is not provable in straight Coq but you can assume it. And while you are at it, if your going to do math, you will also want function extensionality. Both forms of extensionality follow from univalence, which is also an extensionality principle, except that this one is for the universe of types.

If you prefer to avoid all this you can go down the road of setoids: you equip every types with an equivalence relation that serves as the equality relation. You then have to keep proving that your functions preserve these relations. It's a lot of "fun".