Yoneda Lemma

(Yoneda Lemma) Consider a locally small category $C$. For any object $x \in C$ and any (covariant) functor $F : C \rightarrow \Set$, there is a bijection $\Phi$ of sets

$$[C,\Set]( \Hom_C(x,-), F) \cong Fx$$

that associates each natural transformation $\eta : \Hom_C(x,-) \Rightarrow F$ with the element $\Phi(\eta) \equiv \eta_x(\id_x) \in Fx$. Moreover, this correspondence is natural in both $x$ and $F$.

(coYoneda Lemma) Consider a locally small category $C$. For any object $x \in C$ and any contravariant functor $F : C^{op} \rightarrow \Set$, there is a bijection $\Phi$ of sets

$$[C^{op},\Set]( \Hom_C(-,x), F) \cong Fx$$

The (covariant) Yoneda Embedding is the covariant functor

$$\begin{aligned} Y : C &\rightarrow [C^{op}, \Set] \\ x &\mapsto \Hom_C(-,x) & \text{(objects)} \\ (f : x \rightarrow y) &\mapsto (- \fcmp f) & \text{(morphisms)} \end{aligned}$$

sending each object to its contravariant Hom-functor, and each morphism $(f : x \rightarrow y)$ to the natural transformation $(-\fcmp f)$ defined by the $f$-postcomposition.

The morphisms $f : x \rightarrow y$ and $g : y \rightarrow z$ in $C$ are sent by the Yoneda embedding to the natural transformations

$$\begin{aligned} Yf &= (- \fcmp f) : \Hom_C(-,x) \Rightarrow \Hom_C(-,y) \\ Yg &= (- \fcmp g) : \Hom_C(-,y) \Rightarrow \Hom_C(-,z) \\ \end{aligned}$$

We must show $Y(f \fcmp g) = (Yf \fcmp Yg)$, where the composition $(f \fcmp g) : x \rightarrow z$ has image

$$Y(f \fcmp g) = (- \fcmp (f \fcmp g)) : \Hom_C(-,x) \Rightarrow \Hom_C(-,z)$$

whose components $(- \fcmp (f \fcmp g))_c : \Hom_C(c,x) \rightarrow \Hom_C(c,z)$ act on morphisms $h : c \rightarrow x$ as

$$\begin{aligned} \left[ Y (f \fcmp g) \right]_c h &= (- \fcmp (f \fcmp g))_c h \\ &= (h \fcmp (f \fcmp g)) \\ &= ((h \fcmp f)) \fcmp g) \\ &= (- \fcmp g)_x (h \fcmp f) \\ &= (- \fcmp g)_x (- \fcmp f)_c h = [ Yf \fcmp Yg ]_c h \end{aligned}$$

where the middle step relies on associativity of function composition.

For a locally small category $C$, the Yoneda Embedding $Y : C \rightarrow [C^{op},\Set]$ is a [[fully-faithful]] functor, embedding $C$ as a [[full-subcategory]] of $[C^{op}, \Set]$.

In a locally small category, $\Hom_C(x,-) \cong \Hom_C(y,-) \iff x \cong y$.

The contravariant Yoneda Embedding is the contravariant functor

$$\begin{aligned} Y : C^{op} &\rightarrow [C, \Set] \\ x &\mapsto \Hom_C(x,-) & \text{(objects)} \\ (f : x \rightarrow y) &\mapsto (f \fcmp -) & \text{(morphisms)} \end{aligned}$$

sending each object to its covariant [[hom-functor]] and each morphism $(f : x \rightarrow y)$ to the natural transformation $(f \fcmp -)$ defined by $f$-precomposition. The functor $Y$ is [[fully-faithful]] and embeds $C^{op}$ as a [[full-subcategory]] of $[C, \Set]$. Consequently,

$$\Hom_C(x,-) \cong \Hom_C(y,-) \iff x \cong y$$

(Yoneda Embedding) The functors below are full and faithful embeddings.

Let $(P, \leq)$ be a [[preorder]] category, where each hom-set contains at most one morphism, and where each morphism $f : x \rightarrow y$ can be thought of as [[evidence]] that the statement $(x \leq y)$ is true. The Yoneda embedding reads

$$[P, \Set]\bigg( (x \leq -), (y \leq -) \bigg) \cong (y \leq x)$$

Using [[coq]] syntax, the left-hand side is the set of polymorphic functions which convert evidence that $(x \leq z)$ into evidence that $(y \leq z)$, that is,

η : forall z, (x <= z) -> (y <= z)

Yoneda confirms that this proposition is logically equivalent to (y <= x). That is,

$$(y \leq x) \iff \big[ \forall z \in P, (x \leq z) \implies (y \leq z) \big]$$

([Riehl 2017], Cor. 2.2.9) Every row operation on matrices with $n$ rows is defined by left multiplication by some $n \times n$ matrix, namely the matrix obtained by performing the row operation on the identity matrix.

(Cayley's Theorem / [Riehl 2017], Cor. 2.2.10) Every group is isomorphic to a subgroup of a permutation group.

In the category [[hask]], of types and Haskell functions between them,

• a natural transformation is nothing more than a [[polymorphic]] function, and
• the (covariant) [[hom-functor]] $\Hom_C(c,-)$ is expressed by the signature c ->.

Presuming Hask ⊆ Set, the Yoneda Lemma for a functor F : Hask -> Hask reads:

$$[\mathtt{Hask}, \mathtt{Hask}]\left( \code{c ->}, \code{F} \right) \cong \code{F c}$$

In the case of the [[list-functor]], written [ ], we see that a polymorphic function η :: forall x. (c -> x) -> [x] is the same as a list [c]. This makes sense -- if we can produce a list of x's when all we have to work with is a function mapping c -> x, we must have a list of c's stashed away somewhere! Applying η to the identity map id :: c -> c reveals the original list.

Note: We can also use the [[reader-monad]], whose functor instance Reader c is (covariantly) represented by c. The reader monad gives another way to make use of hidden data inside a function!

The signature for η reads like a partially-applied fmap, and this is no coincidence! Given data p :: [c], the Yoneda bijection gives the following implementation for η,

η :: forall x. (c -> x) -> [x]
η f = (fmap f) p 

The Yoneda Lemma tells us that every implementation of this function signature must have the form above, for some specific value of p.

In the category [[hask]], the coYoneda Lemma on the list functor [ ] reads

$$[\mathtt{Hask}, \mathtt{Hask}]\left( \code{-> c}, \code{[ ]} \right) \cong \code{[c]}$$

So a polymorphic function η :: forall x. (x -> c) -> [x] is the same as a list [c], but how? In Hask, naturality means that η is [[parametrically-polymorphic]], in the sense that the formula for η cannot use any specific information about the type x.

The Yoneda bijection tells us how to extract this hidden data from a particular η,

id :: c -> c
id x = x

η(id) :: [c]

In the other direction, each [c] gives rise to an η :: forall x. (x -> c) -> [x],

η :: forall x. (x -> c) -> [x]
η = ... TODO

[[todo]] : explain this example better with the writer monad

List is not a contravariant functor!!!

In the category [[hask]], the Yoneda Embedding reads

$$[\mathtt{Hask}, \mathtt{Hask}]\left( \code{a->}, \code{b->} \right) \cong \code{b->a}$$

meaning that a polymorphic function η :: forall x. (a→x) → (b→x) is equivalent to a function b→a. That is, if we can convert any (a→x) to a (b→x), we must have a function (b→a) stashed away somewhere that we can use before applying the (a→x). Surely enough, applying η to the id :: a → a yields the hidden (b→a)!

Likewise, every polymorphic function η :: forall x. (a→x) → (b→x) has the form

p :: b -> a
p = ...

η :: forall x. (a -> x) -> (b -> x)
η f = p ; f

Following [Milewski 2015], Yoneda applied to the identity functor on Hask says that a polymorphic function η :: forall x. (c -> x) -> x is the same as c. In other words, any type c can be replaced by a function that takes a handler for c.

A handler is a function that accepts a and afterwards performs the rest of some computation -- akin to the [[continuation-passing-style]] used by compilers. In fact,

newtype Cont r a = Cont { runCont :: (a -> r) -> r }