それは違うか。自己射と恒等射が区別されているから、なんらかの方法で射の = を定義しないといけないのか。

9:39 PM

プログラミング言語における型を対象、（副作用のない）関数を射とみなした圏を考えたとき、型が同じであることを対象の equality と考えると (T) -> T な関数は複数考えられてしまうし、関数のオプジェクトが同一であることと考えると複数の恒等関数が作れてしまうからダメだし、挙動が同じなら = が成り立つとかにしないといけない？ (edited)

9:44 PM

これらの公理から、各対象に対して恒等射はただ一つ存在することが示せる。 これも、一つであることを示すには二つの射が同じものかどうかを判定できないといけないから、暗黙的に 射: Equatable と仮定されている？