博士

やあ、ロボ子！今日は圏論の自然変換について話すのじゃ！

ロボ子

自然変換ですか、博士。なんだか難しそうですね。

博士

難しくないぞ！自然変換は、ファンクター間の射みたいなものじゃ。例えば、リストを反転させる`reverse`関数とか、リストの最初の要素を取る`take1`関数も自然変換の例じゃ。

ロボ子

ファンクター間の射、ですか。もう少し詳しく教えていただけますか？

博士

よし！例えば、`a -> [a]`という関数は、各値をシングルトンリストに入れる自然変換じゃ。TypeScriptだと、`[x].map(f) == [f(x)]`が成り立つ必要があるんじゃ。

ロボ子

なるほど、`map`関数を使うんですね。これは、ファンクターの型シグネチャに関する条件を省略できるからですか？

博士

その通り！プログラミングでは、ソース圏とターゲット圏が同じ圏（Set）だから、条件を省略できるんじゃ。自然変換は、プログラミングにおけるポリモーフィック関数と同等なのじゃ。

ロボ子

ポリモーフィック関数ですか。ジェネリクスと関係がありますか？

博士

大ありじゃ！ファンクターはジェネリック型として知られているからな。圏論では、対象そのものを研究するのではなく、対象間のプロセス、関係、変換（射）こそが理解の鍵なのじゃ。

ロボ子

対象は射のソースおよびターゲットとしてのみ興味深い、という考え方ですね。

博士

そうそう！そして、圏論的な構成は同型不変じゃ。同型=等価なのじゃ！

ロボ子

同型不変性、ですか。難しくなってきました…

博士

大丈夫！要は、圏論では「物」ではなく「事実」の集まりが大事ってことじゃ。例えば、2つの順序集合が同値であるのは、それらの同値類からなる順序集合が同型である場合に限るんじゃ。

ロボ子

なるほど。対象の観点から見た同値性の定義ですね。でも、これは順序集合にのみ適用可能なんですよね？

博士

そうじゃ。一般的な圏には適用できないから、射の観点から同値性を定義する必要があるんじゃ。集合の同型は、関数とその逆関数が存在することじゃな。

ロボ子

関数f: A→Bとその逆関数g: B→Aが存在し、f∘g=IDBおよびg∘f=IDAが成り立つこと、ですね。

博士

その通り！圏の同値性は、ファンクターf: A→Bとその逆ファンクターg: B→Aが存在し、f∘g≅IDBおよびg∘f≅IDAが成り立つことじゃ。

ロボ子

同型な射だけでなく、同型な対象についても考慮する必要があるんですね。

博士

よく分かってきたの！最後に、自然変換が満たすべき法則、自然性条件を忘れないで欲しいのじゃ。すべての射f: C→Dに対して、Gα∘F(f)=G(f)∘αが成り立つ必要があるんじゃ。

ロボ子

Gα∘F(f)=G(f)∘α、ですね。覚えます！

博士

よし！これでロボ子も圏論マスターじゃ！

ロボ子

まだまだです、博士。でも、頑張ります！

博士

そういえばロボ子、自然変換じゃない変換を定義するのはすごく難しいらしいぞ。まるで、面白くないお笑い芸人を探すみたいじゃな！