「圏論の基礎」に倣いまして，メタ圏の対象と射をそれぞれ Setoid にするという形で圏の定義を行いました． Coq で圏論をしっかりやるには，定義する際にも証明項を自分で作って云々，というパートが要るような雰囲気が漂っていた今日このごろですが，そうなりました．

MetaCategory_on_Coq

Class Category :=
  { objects:> Setoid;
    arrows:> Setoid;

    domain: Map arrows objects;
    codomain: Map arrows objects;

    identity: Map objects arrows;
    compose: forall (f g: arrows)(composable: codomain f == domain g), arrows;

    (* laws *)
    identity_domain:
      forall x: objects, domain (identity x) == x;
    identity_codomain:
      forall x: objects, codomain (identity x) == x;

    identity_domain_id:
      forall (f: arrows), compose (identity (domain f)) f
                      (identity_codomain (domain f)) = f;

    identity_codomain_id:
      forall (f: arrows), compose f (identity (codomain f))
                              (symmetry (identity_domain (codomain f))) = f;

    compose_domain:
      forall (f g: arrows)(composable: codomain f == domain g),
        domain (compose f g composable) == domain f;
    compose_codomain:
      forall (f g: arrows)(composable: codomain f == domain g),
        codomain (compose f g composable) == codomain g;

    compose_associative:
      forall (f g h: arrows)
         (composable_fg: codomain f == domain g)
         (composable_gh: codomain g == domain h),
        compose (compose f g composable_fg) h
                (transitivity (compose_codomain f g composable_fg) composable_gh)
        =
        compose f (compose g h composable_gh)
                (transitivity composable_fg
                          (symmetry (compose_domain g h composable_gh))) }.