HaskellのCo/Yoneda型と米田の補題をきちんと繋げる - Qiita

概要 Haskell には Co/Yonda 型があり、圏論には米田の補題がある。両者の関連についての分かりやすい解説を見つけられなかったため、ここで米田の補題と Co/Yoneda 型をシームレスに繋ぐことを試みる。 圏論の基礎知識は仮定している。また Co/Yoneda 型は kan-extensions で定義されたものを参照している。 記法 圏論の記法は一般的なものを用いるが、Haskell コードとの比較のし易さのために、圏 $\mathcal C$ における対象 $A$ から対象 $B$ への射の集合 $\mathcal C (A,B)$ を $$ A\underset{\mathcal C}{\rightarrow}B $$ とも書くことにする。 米田の補題 米田の補題によると、圏 $\mathcal C$ とその対象 $A$ ならびに関手 $F:\mathcal C\rig