型クラスの引数に型クラス内部で別名を与えることで，異なる実体に共通の記法を提供するというやり方． 既にやっているライブラリとかもあると思いますが，メモ的な意味で投下．

gistfile1.coq

Definition relation (A: Type) := A -> A -> Prop.

(* Definition: Equivalence relation *)
Reserved Notation "x == y" (at level 80, no associativity).

Class Equivalence {A: Type}(eq: relation A) :=
  {
    equiv_eq := eq
      where "x == y" := (equiv_eq x y);

    equiv_refl:
      forall (a: A), a == a;
    equiv_sym:
      forall (a b: A),
        a == b -> b == a;
    equiv_trans:
      forall (a b c: A),
        a == b -> b == c -> a == c
  }.

Notation "x == y" := (equiv_eq x y) (at level 80, no associativity).


(* Instances *)
Instance eq_Equivalence (A: Type): Equivalence (eq (A:=A)).
Proof.
  split; congruence.
Defined.

Instance iff_Equivalence: Equivalence (fun P Q => P <-> Q).
Proof.
  split; tauto.
Defined.


(* Example *)
Goal
  (forall n m: nat, (n == m) == (S n == S m)).
Proof.
  intros.
  split; congruence.
Qed.  


(*
クラスの書き方を

Class Equivalence (A: Type) :=
  {
    equiv_eq: relation A;
    ...
  }.

としても共通の記法を与えることはできるけど，
宣言時，例えば別のクラスで

 {
    ...
    equivalence: Equivalence A;
    ...
  }

と書くことになる．
これだと同値関係を与えてくれる二項関係の実体を
こちらで明示するのが大変なんですよねー．

*)