%
\label{thm:yoneda-embedding}
The Yoneda functor $y \colon \tau \to [\tau^{\op}, \tau]$
(Definition~\ref{def:yoneda-functor})
is fully faithful.
Concretely:
\begin{enumerate}
    \item \textbf{Well-defined.}
          For each object $A$,
          the representable presheaf $y(A) = [-, A]$
          is a $\tau$-object.
          The functor $y$ is a functor between $\tau$-enriched categories.

    \item \textbf{Faithful.}
          If $y(\varphi) = y(\psi)$
          for morphisms $\varphi, \psi \colon A \to B$,
          then $\varphi = \psi$.

    \item \textbf{Full.}
          Every natural transformation
          $\eta \colon y(A) \Rightarrow y(B)$
          that respects the bipolar sector structure
          is of the form $\eta = y(\varphi)$
          for a unique $\varphi \colon A \to B$.

    \item \textbf{Bipolar preservation.}
          For every morphism $\varphi \colon A \to B$
          with bipolar decomposition
          $\varphi = e_+ \cdot \varphi_+ + e_- \cdot \varphi_-$,
          \[
              y(e_+ \cdot \varphi_+ + e_- \cdot \varphi_-)
              \;=\;
              e_+ \cdot y(\varphi_+) + e_- \cdot y(\varphi_-).
          \]
          The Yoneda embedding preserves the bipolar splitting.
\end{enumerate}

We prove each property in turn.

\medskip
\textbf{(1) Well-definedness.}\;
By self-enrichment (II.D53),
$[P, A]$ is a $\tau$-object
for every pair $(P, A)$.
The assignment $P \mapsto [P, A]$
is contravariant-functorial in $P$
(precomposition is well-defined
by the category structure earned in II.T28).
Therefore $y(A) = [-, A]$
is a functor $\tau^{\op} \to \tau$.
The morphism map $y(\varphi)$
is a natural transformation
by the probe naturality argument
(Lemma~\ref{lem:probe-yoneda}, (PN) $\Rightarrow$ (Yon)).

\medskip
\textbf{(2) Faithfulness.}\;
Assume $y(\varphi) = y(\psi)$
as natural transformations $y(A) \Rightarrow y(B)$.
Evaluate at $P = A$ and $f = \id_A$:
\[
    \varphi
    \;=\; y(\varphi)_A(\id_A)
    \;=\; y(\psi)_A(\id_A)
    \;=\; \psi.
\]
Alternatively, this follows from the Code/Decode bijection (II.T35):
$\mathrm{Code}(\varphi) = \mathrm{Code}(\psi)$
(since $y(\varphi)$ determines the boundary stream of $\varphi$),
and $\mathrm{Code}$ is injective.

\medskip
\textbf{(3) Fullness.}\;
Let $\eta \colon y(A) \Rightarrow y(B)$
be a natural transformation
that respects the bipolar sector structure.
Define
\[
    \varphi \;:=\; \eta_A(\id_A) \;\in\; [A, B].
\]
We claim $\eta = y(\varphi)$.
For any probe $g \colon P \to A$:
\[
    \eta_P(g)
    \;=\; \eta_P\bigl(g^*(\id_A)\bigr)
    \;=\; g^*\bigl(\eta_A(\id_A)\bigr)
    \;=\; \varphi \circ g
    \;=\; y(\varphi)_P(g).
\]
The second equality uses naturality of $\eta$:
\[
    \begin{tikzcd}
        {[A, A]} \ar[r, "{\eta_A}"] \ar[d, "{g^*}"']
        & {[A, B]} \ar[d, "{g^*}"] \\
        {[P, A]} \ar[r, "{\eta_P}"']
        & {[P, B]}
    \end{tikzcd}
\]
commutes, so $\eta_P(g^*(\id_A)) = g^*(\eta_A(\id_A))$.

The morphism $\varphi = \eta_A(\id_A)$ is well-defined
as a $\tau$-morphism
because $\eta$ respects the bipolar structure
and $\id_A$ is bipolar-neutral.
The Code/Decode bijection (II.T35)
provides the computable witness:
$\mathrm{Code}(\varphi)$ is the boundary stream
extracted from $\eta_A(\id_A)$,
and $\mathrm{Decode}(\mathrm{Code}(\varphi)) = \varphi$.

Uniqueness:
if $\eta = y(\varphi) = y(\psi)$,
then $\varphi = \psi$ by faithfulness.

\medskip
\textbf{(4) Bipolar preservation.}\;
Let $\varphi = e_+ \cdot \varphi_+ + e_- \cdot \varphi_-$
be the bipolar decomposition of $\varphi$.
For any probe $g \colon P \to A$:
\[
    y(\varphi)_P(g)
    \;=\; \varphi \circ g
    \;=\; (e_+ \cdot \varphi_+ + e_- \cdot \varphi_-) \circ g
    \;=\; e_+ \cdot (\varphi_+ \circ g) + e_- \cdot (\varphi_- \circ g),
\]
where the last equality uses
the bilinearity of composition
over the idempotent decomposition
(the program monoid respects
the $e_\pm$-splitting, I.P02).
Therefore
\[
    y(\varphi)_P
    \;=\;
    e_+ \cdot y(\varphi_+)_P
    \;+\;
    e_- \cdot y(\varphi_-)_P,
\]
which is the bipolar decomposition of $y(\varphi)$
at each component $P$.