Yoneda / co-Yoneda

• Data.Functor.Yoneda
• Data.Functor.Contravariant.Coyoneda

---

• Yoneda lemma : ∀ b. (a → b) → f b ≅ f a (f : Functor)
• co-Yoneda lemma : ∃ b. (a → b, f b) ≅ f a (f : Contravariant)

左から右に

• (a → b) として id を取れる。a = b より f b = f a が返る。
• a → b より f b → f a が構成できて、f a を生成可能。

右から左に

• λf.fx
• b = a として (id, x)

右から左は明らかに埋め込みなので左から右の逆を示す

• 多相関数なので関数の性質はだいぶ制限されるはず (a → a と a → b の合成として解釈すると id を渡せば十分？函手性)
• 存在は失われるが、同型であることに変わりはない (情報を取り出すには b が既知であるか、contramapしかない)