米田の補題について

先ずはHomo functorの定義:

h(-,C): Cop -> Set

さらに：

h(-): C -> (Cop -> Set)

functor h(-) は米田埋め込み(Yoneda embedding)という名があり、Yと表記される。
米田の補題(Yoneda lemma)は下記となる：

∀F ∈ (Cop -> Set) と ∀A ∈ C, ∃ fA,F: ( h(-,A) -> F ) -> F(A), fA,Fは全単射(bijection/fully faithful)である。更に、この全単射は下記の意味ではCとFの間でnaturalの性質を持つ：

gとμを与える：
g: A' -> A in C
μ: F ⇒ F' in (Cop -> Set), 下図のようにSet中で交換可能の意味を持つ：
                        fA,F
( h(-,A) -> F ) -----------> F(A)
         |                                |
(g, μ)|                                |μA'F(g) = F'(g)μA
       |                                |
     ↓                              ↓
( h(-,A') -> F' )----------> F'(A')
                        fA',F'

抽象過ぎて全く意味分からないのでHaskellにマッピングできるかを試してみた。
まずは h(-,C) を定義する：

data Homo c cop = Homo c cop deriving( Eq, Show )

instance Functor (Homo c) where
  fmap f (Homo c cop) = Homo c (f cop)

この定義ではh(Cop, C)はmorphism:( C -> Cop )の意味合いを表現できないが、今回はこいつをmorphismとして使わないから、morphismであることをこころに留めればいいと思う。
次はF、今回は特殊ケースでFもhomo functorを使うから特にすることがない。
次はfA,F：

-- h(-,A) -> F -> F(A)
bijection :: Homo c cop -> Homo c' cop' -> Homo c' c
bijection (Homo x _) (Homo y _) = Homo y x

正直微妙だね。なぜなら上記の定義から「h(-,A) -> F」がnatural transfermationのことが分からない。
まあ実際はnatural transfermationだけどね(下記μの定義を参照)。
こんな風に：

bijection :: (Homo c -> Homo c') -> Homo c' c

書ければ一番いいのだが、残念な事でできない。
あとはgとμを適当に定義して結果を見るだけだ：

myu :: Homo c cop -> Homo (Homo c c) cop
myu (Homo x y) = Homo (Homo x x) y

main :: IO ()
main = print (bijection (Homo (g "A") "_") (myu (Homo "B" "_"))) >>   -- (1), 図の↓、→ルート
       print (myu . fg $ bijection (Homo "A" "_") (Homo "B" "_")) >>  -- (2), 図の→、↓ルート
       print (f'g . myu $ bijection (Homo "A" "_") (Homo "B" "_"))    -- (3), (1-3) must be equal
         where g = \x->x++"!"
               fg = fmap g
               f'g = fmap g

Output:

Homo (Homo "B" "B") "A!"
Homo (Homo "B" "B") "A!"
Homo (Homo "B" "B") "A!"

おお！素晴らしい！米田さんマジぱねぇっす！シビれるあこがれるゥ！
結論：米田の補題について理解したとは言えないが、少し具体的なイメージを捉えた。一応収穫ありってことね。