米田埋め込みは充満忠実である

目標関手を $F:=h_B$ として米田の補題を適用する。補題は全単射 $\mathrm{Nat}(h_A,h_B)\cong h_B(A)$ を与え、定義 $h_B(A)=\mathrm{Hom}_{\mathcal{C}}(A,B)$ を展開すると、まさに $\mathrm{Nat}(h_A,h_B)\cong\mathrm{Hom}_{\mathcal{C}}(A,B)$ が得られる。

残るは、この全単射のもとで自然変換 $\eta:h_A\Rightarrow h_B$ がどの $\mathcal{C}$ の射に対応するかを特定し、それが後合成であることを確認することである。$\Phi$ の公式により、$\eta$ は元 $\Phi(\eta)=\eta_A(1_A)\in\mathrm{Hom}(A,B)$ に対応する;この射を $f$ と呼ぶ。

次に $\Psi(\Phi(\eta))=\eta$(上の定理を $F=h_B$ に適用したもの)を使って、$\eta$ のすべての成分を $f$ から復元する:任意の対象 $X$ と任意の $g\in h_A(X)=\mathrm{Hom}(X,A)$ について、$\Psi(f)_X(g)=h_B(g)(f)$。$h_B$ の射への反変作用——前合成——を展開すると $h_B(g)(f)=f\circ g$ が得られる。よって $\eta_X(g)=f\circ g$:$\eta$ のすべての成分は文字通り $f$ による後合成である。

$\Phi$ と $\Psi$ が互いに逆な全単射である(上で証明済み)こと、そして $f$ による後合成がまさに $\Psi(f)$ であることから、$f$ を $f$ による後合成に送る割り当ては自体が全単射 $\mathrm{Hom}(A,B)\to\mathrm{Nat}(h_A,h_B)$ である——これがまさに $y$ が充満忠実であるという主張である。