Avatar
この辺りのちゃんとした話は「数学基礎論」という分野できちんと定式化されているはずで、僕はちゃんと勉強したことがないのでまた雰囲気でしか話せませんが、 https://en.m.wikipedia.org/wiki/Zermelo–Fraenkel_set_theory (edited)
11:25 AM
「公理論的集合論」では、 a ∈ A という関係を全ての出発点として集合というものを定義していきます。
11:26 AM
要素の equality の定め方には二つの流儀があるらしく、集合の要素は Equatable だということをはじめから規定しておくか、集合が Equatable であることを使って要素の equality を「定義」することもできるそうです。 (edited)
11:26 AM
11:27 AM
後者の場合は Set<T> の Equatable の定義が先にあって、それを使って T: Equatable を定義している、という感じですね。 (edited)
11:33 AM
圏の話に戻すと、圏の射は Equatable だけど対象は Equatable であるとは仮定されていないんですよね。
11:34 AM
圏の一般論では「対象が同型かどうか」までしか言えず、集合のように「ピタッと一致している」ということは言えないんです。だからこそ普遍性などを使って射によって対象を特定していく、という普通の数学でやってたこととは全く別のアプローチを取ることになります。 (edited)