The Yoneda Lemma: A Theoretical Foundation

The Yoneda Lemma is a fundamental result in category theory, establishing a deep relationship between objects in a category and functors from that category to the category of sets. This document provides a formal definition, proof, and implications of the lemma.

---

1. Prerequisites

• Categories: A category $\mathcal{C}$ consists of objects and morphisms (arrows) satisfying composition and identity laws.
• Functors: A functor $F: \mathcal{C} \to \mathbf{Set}$ maps objects of $\mathcal{C}$ to sets and morphisms to functions.
• Hom-Functor: For a fixed object $A \in \mathcal{C}$, the hom-functor $\mathcal{C}(A, -): \mathcal{C} \to \mathbf{Set} $ sends an object $X$ to the set of morphisms $\mathcal{C}(A, X)$.

---

2. Statement of the Yoneda Lemma

Let:

• $\mathcal{C}$ be a locally small category (i.e., $\mathcal{C}(A, B)$ is a set).
• $F: \mathcal{C} \to \mathbf{Set}$ be a functor.
• $A \in \mathcal{C}$ be an object.

Yoneda Lemma: There is a bijection, natural in both $A$ and $F$:

$$\mathrm{Nat}(\mathcal{C}(A, -), F) \cong F(A)$$

where $\mathrm{Nat}$ denotes the set of natural transformations between the functors.

---

3. Proof of the Yoneda Lemma

Step 1: Define the Bijection

• Given a natural transformation $ \alpha: \mathcal{C}(A, -) \to F$, define $\Phi(\alpha) = \alpha_A(\mathrm{id}_A) \in F(A)$.
• Conversely, given $u \in F(A)$, define $\Psi(u): \mathcal{C}(A, -) \to F$ by:

$$\Psi(u)_X(f) = F(f)(u) \quad \text{for } f \in \mathcal{C}(A, X).$$

Step 2: Verify Naturality

• Check that $\Psi(u)$ is a natural transformation: For any morphism $g: X \to Y$ in $\mathcal{C}$, the following diagram commutes:

$$\begin{array}{ccc} \mathcal{C}(A, X) & \xrightarrow{\Psi(u)_X} & F(X) \\\ \downarrow{g \circ -} & & \downarrow{F(g)} \\\ \mathcal{C}(A, Y) & \xrightarrow{\Psi(u)_Y} & F(Y) \end{array}$$

Step 3: Prove $\Phi$ and $\Psi$ are Inverses

• Show $\Phi(\Psi(u)) = u$ for $u \in F(A)$:

$$\Phi(\Psi(u)) = \Psi(u)_A(\mathrm{id}_A) = F(\mathrm{id}_A)(u) = u.$$

• Show $\Psi(\Phi(\alpha)) = \alpha$ for $ $ \alpha: \mathcal{C}(A, -) \to F$: For any $X$ and $f \in \mathcal{C}(A, X)$,

$$\Psi(\Phi(\alpha))_X(f) = F(f)(\alpha_A(\mathrm{id}_A)) = \alpha_X(f \circ \mathrm{id}_A) = \alpha_X(f).$$

---

4. Corollaries and Implications

Corollary 1 (Yoneda Embedding)

The functor:

$$\mathcal{C}^{\mathrm{op}} \to \mathbf{Fun}(\mathcal{C}, \mathbf{Set}), \quad A \mapsto \mathcal{C}(A, -)$$

is fully faithful. This embeds $\mathcal{C}$ into the category of contravariant functors.

Corollary 2 (Uniqueness up to Iso)

If $\mathrm{Nat}(\mathcal{C}(A, -), \mathcal{C}(B, -)) \cong \mathcal{C}(B, A)$, then $A$ and $B$ are isomorphic if and only if their hom-functors are naturally isomorphic.

---

5. Example in Haskell

The Yoneda Lemma underlies "Yoneda embedding" in functional programming:

data Yoneda f a = Yoneda (forall b. (a -> b) -> f b)