対象と射と射の equality を決めてそれが条件を満たせば圏になるわけですね。射の equality が必要なのは射の合成や結合律、単位律の中から読み取れると。なんだか Structural Subtyping みたいですね。