Feeling The Yoneda Lemma in my Guts

Category theory confession time: I've known about the Yoneda lemma for a long time, and never really felt like I got it. Went through the proof I don't know how many times, never found anything mysterious about it, but never really had any intuition for what it meant beyond some mumbling about Cayley groups and stuff.

But something finally clicked into place for me some months ago after seeing Fosco Loregian's awesome This is the (co)end, my only (co)friend, right where he talks about the end/coend Yoneda-lemma corollaries he calls the "Ninja Yoneda Lemma", Proposition 2.1. In his notation, it's the statement of four natural isomorphisms of functors,

\[(i)\ K \cong \int^c Kc \x \C(\_, c)\]	\[(ii)\ K \cong \int_c Kc^{ \C(c, \_)}\]
\[(iii)\ H \cong \int^c Hc \x \C(c, \_)\]	\[(iv)\ H \cong \int_c Hc^{ \C(\_, c)}\]

for any $K : \rset^{\C^\op}$ and any $H : \rset^{\C}$, where $\int^c$ stands for the coend over every object $c \in \C$, and $\int_c$ stands for the end over every object $c\in \C$.

The thing that clicked for me was first seeing these as logical equivalences, as if they were saying

\[(i)\ K \prequiv \exists c . Kc \land \C(\_, c)\]	\[(ii)\ K \prequiv \forall c . \C(c, \_) \imp Kc\]
\[(iii)\ H \prequiv \exists c . Hc \land \C(c, \_)\]	\[(iv)\ H \prequiv \forall c. \C(\_, c) \imp Hc\]

and realizing that the role the homset $\C(\_, \_)$ is playing is in fact one of directed equality. For the following equivalences are absolutely provable in first-order logic:

\[(i)\ K(x) \prequiv \exists c . K(c) \land (x = c)\]	\[(ii)\ K(x) \prequiv \forall c . (c = x) \imp K(c)\]
\[(iii)\ H(x) \prequiv \exists c . H(c) \land (c = x)\]	\[(iv)\ H(x) \prequiv \forall c. (x = c) \imp H(c)\]

And indeed $(i)$ and $(iii)$ are the same, and $(ii)$ and $(iv)$ are the same, up to the symmetry of equality.

All of $(i)/(ii)/(iii)/(iv)$ contain the essential information of both the introduction and elimination rules of equality. The elim rule in plain english is the fact that

The only thing that is equal to $x$ is $x$ itself.

and the intro rule is the fact that

There is a thing that equal to $x$, namely $x$ itself.

To prove any of these logical equivalences, we use the intro rule for equality when proving the direction that decomposes the quantifier synchronously (i.e. $K(x) \prov \exists c . K(c) \land (x = c)$ or $ \forall c . (c = x) \imp K(c) \prov K(x)$) by choosing $c$ to be $x$ and establishing the resulting reflexive equality. And we use the elim rule when proving the direction that decomposes the quantifer asynchronously (i.e $\exists c . K(c) \land (x = c) \prov K(x)$ or $ K(x) \prov \forall c . (c = x) \imp K(c)$) by using the equality to collapse the two free term variables into one, and then trivially proving $K(c) \prov K(c)$.

Anyway the punchline for me is that the Yoneda lemma is really telling us a certain formal way in which

the hom-type is a directed generalization of equality

and this is true for categories, not just groupoids.