JMeq的なやつといろいろ使って，関数全体を Setoid に仕立てあげた．が，此処から先に進めない． おそらく，Setoid と言いつつキャリアが Type であることが超問題なのであろーう．

function_setoid

  (* Cat_on_Coq の Setoid を使ってるよ *)

  Inductive function_eq {X Y: Set}(f: X -> Y): forall (X' Y': Set)(g: X' -> Y'), Prop :=
  | feq_def: forall f': X -> Y, (forall x: X, f x = f' x) -> function_eq f f'.

  Lemma function_eq_refl:
    forall (Xf Yf: Set)(f: Xf -> Yf),
      function_eq f f.
  Proof.
    move => Xf Yf f.
    by apply feq_def.
  Qed.

  Lemma function_eq_sym:
    forall (Xf Yf Xg Yg: Set)(f: Xf -> Yf)(g: Xg -> Yg),
      function_eq f g -> function_eq g f.
  Proof.
    move => Xf Yf Xg Yg f g Heq.
    induction Heq; apply feq_def; auto.
  Qed.

  Lemma function_eq_trans:
    forall (Xf Yf Xg Yg Xh Yh: Set)(f: Xf -> Yf)(g: Xg -> Yg)(h: Xh -> Yh),
      function_eq f g -> function_eq g h -> function_eq f h.
  Proof.
    move => Xf Yf Xg Yg Xh Yh f g h Heqfg.
    induction Heqfg; subst; auto.
    move => Heqgh.
    induction Heqgh; subst; auto.
    apply feq_def.
    congruence.
  Qed.


  Inductive functions: Type :=
  | functions_def: forall (X Y: Set)(f: X -> Y), functions.
  
  Definition eq_functions (f g: functions): Prop :=
    match f, g with 
      | functions_def X Y f', functions_def X' Y' g' =>
        function_eq f' g'
    end.

  Program Instance eq_functions_Equivalence: Equivalence eq_functions.
  Next Obligation.
    rewrite /Reflexive /eq_functions; move => [X Y f].
    apply function_eq_refl.
  Qed.
  Next Obligation.
    rewrite /Symmetric /eq_functions; move => [Xf Yf f] [Xg Yg g].
    apply function_eq_sym.
  Qed.
  Next Obligation.
    rewrite /Transitive /eq_functions; move => [Xf Yf f] [Xg Yg g] [Xh Yh h].
    apply function_eq_trans.
  Qed.

  Program Instance FunctionSetoid: Setoid :=
    { carrier := functions;
      equal := eq_functions }.