自己函数は合成で以ってモノイドを成すよ。

endo_monoid.v

Set Implicit Arguments.
Unset Strict Implicit.

Require Import Setoids.Setoid Morphisms.

Delimit Scope cat_scope with cat.
Open Scope cat_scope.

Class Setoid :=
  {
    carrier: Type;
    equal: carrier -> carrier -> Prop;
    prf_Setoid: Equivalence equal
  }.
Coercion carrier: Setoid >-> Sortclass.
Coercion prf_Setoid: Setoid >-> Equivalence.
Existing Instance prf_Setoid.
Notation "(== :> X )" := (equal (Setoid:=X)).
Notation "(==)" := (==:>_) (only parsing).
Notation "x == y :> X" := (equal (Setoid:=X) x y) (at level 90, no associativity).
Notation "x == y" := (equal x y) (at level 90, no associativity, only parsing).

Class Monoid :=
  {
    monoid_setoid: Setoid;
    monoid_binop: monoid_setoid -> monoid_setoid -> monoid_setoid
    where "x * y" := (monoid_binop x y);
    monoid_unit: monoid_setoid;

    monoid_binop_subst: Proper ((==) ==> (==) ==> (==)) monoid_binop;
    monoid_assoc:
      forall x y z: monoid_setoid,
        (x * y) * z == x * (y * z);
    monoid_unit_l:
      forall x,
        monoid_unit * x == x;
    monoid_unit_r:
      forall x,
        x * monoid_unit == x
  }.
Coercion monoid_setoid: Monoid >-> Setoid.
Notation "x * y" := (monoid_binop x y): cat_scope.

Instance function (X Y: Type): Setoid | 100 :=
  {
    carrier := X -> Y;
    equal f g := forall x, f x = g x
  }.
Proof.
  split.
  - intros f x; auto.
  - intros f g Heq x; auto.
  - intros f g h Heqfg Heqgh x.
    rewrite Heqfg; apply Heqgh.
Defined.

Instance Endo (X: Type): Monoid :=
  {
    monoid_setoid := function X X;
    monoid_binop f g := fun x => g (f x);
    monoid_unit := fun x: X => x
  }.
Proof.
  - intros f g Heq f' g' Heq' x.
    now rewrite Heq, Heq'.
  - now simpl; intros.
  - now simpl; intros.
  - now simpl; intros.
Defined.

(* Example *)
Check ((S:Endo nat) * S * plus 3): Endo nat.
(* (S:Endo nat) * S * plus 3:Endo nat *)
(*      : Endo nat *)

Check ((plus 1: Endo nat) * mult 3 * plus 2 * mult 4 * plus 1).
(* (plus 1:Endo nat) * mult 3 * plus 2 * mult 4 * plus 1 *)
(*      : Endo nat *)

Compute ((plus 1: Endo nat) * mult 3 * plus 2 * mult 4 * plus 1) 0.
     (* = 21 *)
     (* : nat *)