Yoneda functor

@Deprecated

替わりに(Co)Yoneda reduction for free - PSを参照。

Haskell(kan-extensions)のYoneda functor*1:

module Data.Functor.Yoneda
...
newtype Yoneda f a = Yoneda { runYoneda :: forall b. (a -> b) -> f b }

を攻略する試み。

Contravariant Yoneda embedding

まず、Yoneda embeddingのcontravariant版を定義する:

$\text{y}'\ :\ \mathcal{C}^{\text{op}} \rightarrow \mathcal{Set}^{\mathcal{C}}$
$\text{y}'(x) = \left( \text{Hom}_{\mathcal{C}}(x,\ y) \right)_y$

Covariant Yoneda lemma

Category Theory (Oxford Logic Guides) のYoneda lemmaにおいて

$({\mathcal{C}^{\text{op}})^{\text{op}} = \mathcal{C}$
$\text{Hom}_{\mathcal{C}^{\text{op}}}(Y,\ X) = \text{Hom}_{\mathcal{C}}(X,\ Y)$

を使えば、そのcovariant版を作ることができる:

$\text{Hom}_{ \mathcal{Set}^{\mathcal{C} } }( \text{y}'A,\ F) \simeq FA$

こちらをCovariant Yoneda lemma、Category Theory (Oxford Logic Guides) にあるのをContravariant Yoneda lemmaと勝手に呼ぶことにする*2。 Covariant版の方が、opposite categoryを作るのがめんどうな場合、都合がよさそうである。

Covariant Yoneda functor

Covariant Yoneda lemmaにより、

$\text{Hom}_{ \mathcal{Set}^{\mathcal{C} } }(\text{-},\ F) \circ \text{y}' \simeq F$

となるが、左側のfunctor

$\text{Yoneda}_F = \text{Hom}_{ \mathcal{Set}^{\mathcal{C} } }(\text{-},\ F) \circ \text{y}'$

が

newtype Yoneda f a = Yoneda { runYoneda :: forall b. (a -> b) -> f b }

instance Functor (Yoneda f) where
  fmap f m = Yoneda (\k -> runYoneda m (k . f))

だ、ということ。

f:id:mbps:20131021222558p:plain

Contravariant Yoneda functor

全く同様にして、contravariant版、つまり、Category Theory (Oxford Logic Guides) のYoneda lemmaに対応するものを作ることが出来る。

module Data.Functor.Contravariant.Yoneda
...
newtype Yoneda f a = Yoneda { runYoneda :: forall r. (r -> a) -> f r }

instance Contravariant (Yoneda f) where
  contramap ab (Yoneda m) = Yoneda (m . fmap ab)