(This is more commonly known in category theory
as the “Yoneda lemma” (Wikipedia, nlab, Milewski).)
Given
- A category $\catd$;
- An object $d \in\catd$ such that $(\forall d'\in\catd)\,(\homst d \catd {d'} \in \Set)$
(in this context such objects $d$ are called admissible),
so that the functor $\homst d \catd -$ lands in $\Set$: $\homst d \catd - : \catd \mathrel\longrightarrow \Set$; - A functor $\target {X : {}} \catd \mathrel{\target\longrightarrow} \Set$;
This lemma is proved in a series of four sublemmas, interspersed with some remarks.
Parts of the proof are presented in three different styles,
which are named and described in the left column below,
with examples of these styles in the next two columns.
In the column headed “Unambiguous notation”, upper corner brackets denote “name of”.
However, to reduce notational clutter, in other parts of this document all those corner brackets are omitted
(relying on the wisdom of the reader to understand the proper meaning of the symbol),
as in the examples in the column headed “Ambiguous notation” (i.e., “Overloaded entity names”),
which use the same symbol “$x$” for:
an element of $X_d$, its name, and the name of that.
The last column shows 0-D, 1-D, and 2-D notations for a natural transformation.
Constants used are: $1\in\Set$, the unit (terminal) set, and $\cati\in\CAT$, the unit (terminal) category.
| Style | Unambiguous notation | Ambiguous notation | Notation for natural transformations | |||
|---|---|---|---|---|---|---|
| 0-D (i.e., an element of a set, in set theory) | $x\in X_d$ | $x\in X_d$ | $\tau \in \hom {\homst d \catd -} {[\catd,\Set]} {\target X}$ | |||
| 1-D (i.e., an arrow (1-cell) in a 1-category, in the next two columns $\Set$, in the last column $[\catd, \Set]$) | $1 \xrightarrow[]{\textstyle \ulcorner x \urcorner} X_d$ | $1 \xrightarrow[]{\textstyle x} X_d$ | $\homst d \catd - \buildrel \textstyle \tau \over \Rightarrow \target X$ | |||
| 2-D (i.e., a 2-cell in a 2-category, in this case $\CAT$) ($\ulcorner X_d\urcorner$ and $X_d$ are shown in both unfactored and factored 1-D form) | $\begin{smallmatrix}{} & & \xrightarrow[]{\textstyle \ulcorner 1 \urcorner} \\ & & \textstyle\big\Downarrow\rlap{\textstyle \ulcorner\ulcorner x \urcorner\urcorner} & & \\ \textstyle\cati \mkern{10mu} & & \xrightarrow[\textstyle\ulcorner X_d \urcorner]{} & & \mkern{30mu} \textstyle\Set \\ & \llap{\lower3pt\hbox{$\ulcorner d \urcorner$}}\textstyle\searrow & \Vert & \textstyle\nearrow\rlap{\lower3pt\hbox{$X$}} \\ & & \textstyle\catd \\ \end{smallmatrix}$ | $\begin{smallmatrix}{} & & \xrightarrow[]{\textstyle 1 } \\ & & \textstyle\big\Downarrow\rlap{\textstyle x } & & \\ \textstyle\cati \mkern{10mu} & & \xrightarrow[\textstyle X_d ]{} & & \mkern{10mu} \textstyle\Set \\ & \llap{\lower3pt\hbox{$d$}}\textstyle\searrow & \Vert & \textstyle\nearrow\rlap{\lower3pt\hbox{$X$}} \\ & & \textstyle\catd \\ \end{smallmatrix}$ | $\catd \twocellctb \tau {\homst d \catd -} {\target X} \Set$ |
In applications of this lemma, it is useful to have a notation which indicates
the data to which it is being applied.
The notation used in this and related documents to indicate such
is illustrated by the following example, which refers to the generic data in the statement of the lemma
\[ \text{iaf}(\cati \buildrel \textstyle d \over \longrightarrow \catd \buildrel \textstyle X \over \longrightarrow \Set)\; .\]
Sublemma. Defining the inverse functions of the bijection.
| $\text{restriction}\,\check{()}$ $\hom {\homst d \catd -} {[\catd,\Set]} {\target X} \ni \tau \longmapsto \check\tau \in {\target X}_d\;$(“$\tau-\text{res}$”) | $\text{extension}\,\hat{()}$ ${\target X}_d \ni x \longmapsto \hat x \in \hom {\homst d \catd -} {[\catd,\Set]} {\target X}\;$(“$x-\text{ext}$”) | ||||||
|---|---|---|---|---|---|---|---|
| \[\bbox[20px,border:4px groove red]{\begin{array}{} \cati & \xlongequal{} & \cati\\ \llap{d}\Big\downarrow & \Big\Downarrow\rlap{1_d} & \Big\downarrow\rlap{1}\\ \catd & \twocellctb \tau {\homst d \catd -} {\target X} & \Set \\ \end{array}} \taglabel{iaf-res-2D}\] | \[\bbox[20px,border:4px groove red]{\begin{array}{} \cati & \xlongequal{} & \cati\\ \llap{d'}\Bigg\downarrow \mkern{-10mu} \buildrel \textstyle \delta \over \Longleftarrow \mkern{-10mu} \Bigg\downarrow\rlap{d} & \Big\Downarrow\rlap x & \Bigg\downarrow\rlap{1}\\ \catd & \target{\xrightarrow[\textstyle X]{}} & \Set \\ \end{array}} \taglabel{iaf-ext-2D}\] | ||||||
| The restriction direction $\check{()}$ of bijection $\eqref{iaf-bij}$ is the following composite:
\[\begin{array}{}
\tau \in & \hom {\homst d \catd -} {[\catd,\Set]} {\target X}\\
& \mkern{40mu} \Big\downarrow \mkern{-51mu} \hom {\homst d \catd -} {[d,\Set]} {\target X}\\
d\tau \in & \hom {\homst d \catd d} {[\cati,\Set]} {\target{X}_d} & \cong & \hom {\homst d \catd d} \Set {\target{X}_d} & \ni \tau_d\\
& & & \mkern{30mu} \Big\downarrow \mkern{-36mu} \hom {1_d} \Set {{\target X}_d}\\
& & 1_d\tau_d \in & \hom 1 \Set {{\target X}_d} & \cong & {\target X}_d & \ni (1_d)\tau_d = \bbox[2px,border:2px groove black]{\check\tau}\\
& \textrm{2-D} & & \textrm{1-D} & & \textrm{0-D} & \\
\end{array}\]
This gives (1.46) of Max Kelly’s Basic Concepts of Enriched Category Theory
Note that we restrict/evaluate twice: |
The extension direction $\hat{()}$ of bijection $\eqref{iaf-bij}$ is defined as follows. Given $(x\in \target X_d)$ and $(d' \in \catd)$, define a function in $\Set$ ((the $d'$-part of) the orbit of $x$ under the action $X : \catd \rightarrow \Set$) \[\bbox[10px,border:2px groove black]{ \begin{array}{} \homst d \catd {d'} & \buildrel \textstyle \hat x _{d'} \over \longrightarrow & \target X _{d'}\\ \delta & \longmapsto & (x)\target X_\delta \equiv x\delta \equiv (\delta)\hat x _{d'} \\ \end{array}}\] by \[\begin{array}{} \delta & \in & \homst d \catd {d'}\\ & & \Big\downarrow \mkern{-21mu} \homst d {\target X} {d'}\\ \target X_\delta & \in & \hom {\target X _d} \Set {\target X_{d'}}\\ & & \mkern{20mu} \Big\downarrow \mkern{-30mu} \hom x \Set {\target X_{d'}}\\ x\target X_\delta & \in & \hom 1 \Set {\target X_{d'}} & \cong & \target X _{d'} & \ni & (x)\target X_\delta \equiv x\delta \equiv \bbox[2px,border:2px groove black]{(\delta)\hat x _{d'}} \; .\\ & & \textrm{1-D} & & \textrm{0-D} & &\\ \end{array}\] This is (1.47) of Kelly’s Basic Concepts of Enriched Category Theory when (the base for enrichment $\cal V$) is $\Set$; thus, (the $\eta$ in ECT (1.47)) is (our $x$). $\hat x_{d'}$ is natural in $d'\in\catd$ first over ($d'\in\catd$), then over ($\delta\in \homst d \catd {d'}$). | ||||||
| We can present the definitions, in the form of, effectively, lambda abstraction over elements ($\tau \in \hom {\homst d \catd -} {[\catd,\Set]} {\target X}$), ($x\in X_d$), ($d' \in \catd$), ($\delta \in \homst d \catd {d'}$) in the respective domains, in 0-D, 1-D, and 2-D forms, facilitating comparison. | |||||||
| $\textrm{0-D}$ | $(1_d)\tau_d$ | $\xlongequal{\textstyle\check{()}}$ | $\boxed{\check\tau}$ | $(x)\target X_\delta \equiv x\delta$ | $\xlongequal{\textstyle\hat{()}}$ | $\boxed{(\delta)\hat x_{d'}}$ | |
| $\textrm{1-D}$ (in $\Set$) | $\bbox[20px,border:4px groove black]{1 \xrightarrow[]{\textstyle 1_d} \hom d \catd d \xrightarrow[]{\textstyle \tau_d} \target X_d}$ | $\xlongequal{\textstyle\check{()}}$ | $\bbox[20px,border:4px groove black]{1 \xrightarrow[]{\textstyle \boxed{\check\tau}} \target X_d}$ | $\bbox[20px,border:4px groove black]{1 \xrightarrow[]{\textstyle x} \target X_d \xrightarrow[]{\textstyle \target X_\delta} \target X_{d'}}$ | $\xlongequal{\textstyle\hat{()}}$ | $\bbox[20px,border:4px groove black]{1 \xrightarrow[]{\textstyle \delta} \hom d \catd {d'} \xrightarrow[]{\textstyle \boxed{\hat x_{d'}}} \target X_{d'}}$ | |
| $\textrm{2-D}$ (in $\CAT$) | $\bbox[20px,border:4px groove black]{\begin{array}{} \cati & \xlongequal{} & \cati\\ \llap{d}\Big\downarrow & \Big\Downarrow\rlap{1_d} & \Big\downarrow\rlap{1}\\ \catd & \twocellctb \tau {\homst d \catd -} {\target X} & \Set \\ \end{array}}$ | $\xlongequiv{\textstyle\check{()}}$ | \[\bbox[20px,border:4px groove black]{\begin{array}{} \cati & \xlongequal{} & \cati\\ \llap{d}\Big\downarrow & \Big\Downarrow\rlap{\boxed{\check\tau}} & \Big\downarrow\rlap{1}\\ \catd & \target{\xrightarrow[\textstyle X]{}} & \Set \\ \end{array}}\] | $\bbox[20px,border:4px groove black]{\begin{array}{} \cati & \xlongequal{} & \cati\\ \llap{d'}\Bigg\downarrow \mkern{-10mu} \buildrel \textstyle \delta \over \Longleftarrow \mkern{-10mu} \Bigg\downarrow\rlap{d} & \Big\Downarrow\rlap x & \Bigg\downarrow\rlap{1}\\ \catd & \target{\xrightarrow[\textstyle X]{}} & \Set \\ \end{array}}$ | $\xlongequiv{\textstyle\hat{()}}$ | \[\bbox[20px,border:4px groove black]{\begin{array}{} \cati & \xlongequal{} & \cati\\ \llap{d'}\Big\downarrow & \Big\Downarrow\rlap\delta & \Big\downarrow\rlap{1}\\ \catd & \twocellctb {\boxed{\hat x}} {\homst d \catd -} {\target X} & \Set \\ \end{array}} \] | |
Sublemma. Restriction $\check{()}$ and extension $\hat{()}$ are inverse to each other, i.e.,
$\check{\hat x} = x$ ($x$ extended $\hat{()}$ then restricted $\check{()}$ equals $x$), and
$\hat{\check \tau} = \tau$ ($\tau$ restricted $\check{()}$ then extended $\hat{()}$ equals $\tau$).
The easy proof that $\check{\hat x} = x$ is left as an exercise.
To prove $\hat{\check \tau} = \tau$,
let ($d' \in \catd$) and ($\delta \in \hom d \catd {d'}$) be arbitrary
and consider the following commutative diagram in $\Set$
\[\begin{array}{}
&&\xrightarrow{\displaystyle \check\tau}\\
1 & \xrightarrow{\textstyle 1_d} & \hom d \catd d & \xrightarrow{\textstyle \tau_d} & {\target X}_d\\
& \llap{\mkern{4mu}\lower3pt\delta} \searrow & \mkern{10mu}\bigg\downarrow \mkern{-22mu}\hom d \catd \delta & \tau_\delta & \mkern{6mu}\bigg\downarrow \mkern{-15mu} {\target X}_\delta\\
&& \hom d \catd {d'} & \xrightarrow[\textstyle \tau_{d'}]{} & {\target X}_{d'}
\end{array} \taglabel{iaf-res-ext-1D}\]
where the triangle is the left unit law for $\delta$
and the square is the naturality of $\tau$ at $\delta$.
The top edge of the diagram is $\check \tau$ ($\tau$ restricted);
the top and right edges give $(\delta)(\hat{\check \tau})_{d'}$;
the left and bottom edges give $(\delta)\tau_{d'}$;
so commutativity of the diagram gives $(\delta)(\hat{\check \tau})_{d'} = (\delta)\tau_{d'}$.
Since ($d' \in \catd$) and ($\delta \in \hom d \catd {d'}$) were arbitrary, this gives $\tau = \hat{\check \tau}$.
The crucial diagram $\eqref{iaf-res-ext-1D}$ is the projection of a 2-diagram in $\CAT$: \[\begin{array}{} & & \xrightarrow{\textstyle 1} \\ & & \big\Downarrow \rlap{1_d} \\ \cati & \twocellctb \delta d {d'} & \catd & \twocellctb \tau {\homst d \catd -} {\target X} & \Set \\ \end{array} \taglabel{iaf-res-ext-2D}\]
We can put both parts of the proof of the bijection in either equational (0-D) form
or as equalities between 2-cells in $\CAT$ (2-D) form,
as well as the 1-D form:
| $\textrm{0-D}$ | $\check{\hat x}$ | $\xlongequal{\textstyle\check{()}}$ | $(1_d){\hat x}_d$ | $\xlongequal{\textstyle\hat{()}}$ | $(x)\target X_{1_d} \equiv x\mkern{1mu}1_d$ | $\xlongequal{\target{X^\circ}+\textrm{unit}}$ | $x$ | ||
|---|---|---|---|---|---|---|---|---|---|
| $\textrm{1-D}$ (in $\Set$) | $1$ | $=$ | $1$ | $=$ | $1$ | $=$ | $1$ | ||
| $\downarrow \rlap{1_d}$ | $\downarrow \rlap{x}$ | ||||||||
| $\downarrow \rlap {\check{\hat x}}$ | $\xlongequal{\textstyle\check{()}}$ | $\hom d \catd d$ | $\xlongequal{\textstyle\hat{()}}$ | $\target X_d$ | $\xlongequal{\target{X^\circ}+\textrm{unit}}$ | $\downarrow \rlap x$ | |||
| $\downarrow \rlap{{\hat x}_d}$ | $\downarrow \rlap{\target X_{1_d}}$ | ||||||||
| $\target X_d$ | $=$ | $\target X_d$ | $=$ | $\target X_d$ | $=$ | $\target X_d$ | |||
| $\textrm{2-D}$ (in $\CAT$) | \[\bbox[20px,border:4px groove black]{\begin{array}{} \cati & \xlongequal{} & \cati\\ \llap{d}\Big\downarrow & \Big\Downarrow\rlap {\check{\hat x}} & \Big\downarrow\rlap{1}\\ \catd & \target{\xrightarrow[\textstyle X]{}} & \Set \\ \end{array}}\] | $\xlongequiv{\textstyle\check{()}}$ | \[\bbox[20px,border:4px groove black]{\begin{array}{} \cati & \xlongequal{} & \cati\\ \llap{d}\Big\downarrow & \Big\Downarrow\rlap{1_d} & \Big\downarrow\rlap{1}\\ \catd & \twocellctb {\hat x} {\homst d \catd -} {\target X} & \Set \\ \end{array}}\] | $\xlongequiv{\textstyle\hat{()}}$ | \[\bbox[20px,border:4px groove black]{\begin{array}{} \cati & \xlongequal{} & \cati\\ \llap{d}\Bigg\downarrow \mkern{-10mu} \buildrel \textstyle 1_d \over \Longleftarrow \mkern{-10mu} \Bigg\downarrow\rlap{d} & \Bigg\Downarrow\rlap x & \Bigg\downarrow\rlap{1}\\ \catd & \target{\xrightarrow[\textstyle X]{}} & \Set \\ \end{array}}\] | $\xlongequiv{\target{X^\circ}+\textrm{unit}}$ | \[\bbox[20px,border:4px groove black]{\begin{array}{} \cati & \xlongequal{} & \cati\\ \llap{d}\Big\downarrow & \Big\Downarrow\rlap x & \Big\downarrow\rlap{1}\\ \catd & \target{\xrightarrow[\textstyle X]{}} & \Set \\ \end{array}}\] | ||
| $\textrm{0-D}$ | $(\delta)(\hat{\check \tau})_{d'}$ | $\xlongequal{\textstyle\hat{()}}$ | $(\check\tau){\target X}_\delta$ | $\xlongequal{\textstyle\check{()}}$ | $\bigl((1_d)\tau_d\bigr){\target X}_\delta$ | $\xlongequal{\textstyle 1_d\tau_\delta}$ | $\bigl((1_d) \hom d \catd \delta\bigr) \tau_{d'}$ | $\xlongequal{\textrm{unit}}$ | $(\delta){\target \tau}_{d'}$ |
|---|---|---|---|---|---|---|---|---|---|
| $\textrm{1-D}$ (in $\Set$) | $1$ | $=$ | $1$ | $=$ | $1$ | $=$ | $1$ | $=$ | $1$ |
| $\downarrow\rlap{1_d}$ | $=$ | $\downarrow\rlap{1_d}$ | |||||||
| $\downarrow\rlap\delta$ | $\downarrow\rlap{\check\tau}$ | $\check\tau$ | $\hom d \catd d$ | $=$ | $\hom d \catd d$ | $\textrm{unit}$ | $\downarrow\rlap\delta$ | ||
| $\hat{\check \tau}$ | $\downarrow\rlap{\tau_d}$ | $\downarrow\rlap{\hom d \catd \delta}$ | |||||||
| $\homst d \catd {d'}$ | $\target X_d$ | $=$ | $\target X_d$ | $\tau_\delta$ | $\hom d \catd {d'}$ | $=$ | $\hom d \catd {d'}$ | ||
| $\downarrow\rlap{(\hat{\check \tau})_{d'}}$ | $\downarrow\rlap{\target X_\delta}$ | $=$ | $\downarrow\rlap{\target X_\delta}$ | $\downarrow\rlap{\tau_{d'}}$ | $=$ | $\downarrow\rlap{\tau_{d'}}$ | |||
| $\target X_{d'}$ | $=$ | $\target X_{d'}$ | $=$ | $\target X_{d'}$ | $=$ | $\target X_{d'}$ | $=$ | $\target X_{d'}$ | |
| $\textrm{2-D}$ (in $\CAT$) | \[\bbox[20px,border:4px groove black]{\begin{array}{} \cati & \xlongequal{} & \cati\\ \llap{d'}\Big\downarrow & \Big\Downarrow\rlap\delta & \Big\downarrow\rlap{1}\\ \catd & \twocellctb {\hat{\check \tau}} {\homst d \catd -} {\target X} & \Set \\ \end{array}} \] | $\xlongequiv{\textstyle\hat{()}}$ | \[\bbox[20px,border:4px groove black]{\begin{array}{} \cati & \xlongequal{} & \cati\\ \llap{d'}\Bigg\downarrow \mkern{-10mu} \buildrel \textstyle \delta \over \Longleftarrow \mkern{-10mu} \Bigg\downarrow\rlap{d} & \Big\Downarrow\rlap {\check\tau} & \Bigg\downarrow\rlap{1}\\ \catd & \target{\xrightarrow[\textstyle X]{}} & \Set \\ \end{array}} \] | $\xlongequiv{\textstyle\check{()}}$ | \[\bbox[20px,border:4px groove black]{\begin{array}{} \cati & \xlongequal{} & \cati\\ \llap{d'}\Bigg\downarrow \mkern{-10mu} \buildrel \textstyle \delta \over \Longleftarrow \mkern{-10mu} \Bigg\downarrow\rlap{d} & \Bigg\Downarrow\rlap{1_d} & \Big\downarrow\rlap{1}\\ \catd & \twocellctb \tau {\homst d \catd -} {\target X} & \Set \\ \end{array}} \] | $\xlongequal{\textstyle 1_d\tau_\delta}$ | \[\bbox[20px,border:4px groove black]{\begin{array}{} \cati & \xlongequal{} & \cati\\ \llap{d'}\Bigg\downarrow \mkern{-10mu} \buildrel \textstyle \delta \over \Longleftarrow \mkern{-10mu} \Bigg\downarrow\rlap{d} & \buildrel \textstyle 1_d \over \Longleftarrow & \Big\downarrow\rlap{1}\\ \catd & \twocellctb \tau {\homst d \catd -} {\target X} & \Set \\ \end{array}} \] | $\xlongequiv{\textrm{unit}}$ | \[\bbox[20px,border:4px groove black]{\begin{array}{} \cati & \xlongequal{} & \cati\\ \llap{d'}\Big\downarrow & \Big\Downarrow\rlap\delta & \Big\downarrow\rlap{1}\\ \catd & \twocellctb \tau {\homst d \catd -} {\target X} & \Set \\ \end{array}} \] |
Sublemma. $\hat x_{d'}$ is natural in $d' \in \catd$.
\[\begin{array}{rcccl} \text{If} & d' & \xrightarrow{\textstyle \epsilon} & d'' & \text{is an arbitrary arrow in $\catd$}\\ \text{then} & \text{the} & \text{following} & \text{diagram} & \text{commutes:}\\ \delta \in & \hom d \catd {d'} & \xrightarrow{\textstyle \hom d \catd \epsilon} & \hom d \catd {d''} & \ni \delta\epsilon\\ & \mkern{10mu} \bigg\downarrow \mkern{-22mu} \hom d {\target X} {d'} & \target{\tilde X} & \mkern{10mu} \bigg\downarrow \mkern{-22mu} \hom d {\target X} {d''}\\ {\target X}_\delta \in & \hom {{\target X}_d} \Set {{\target X}_{d'}} & \xrightarrow{\textstyle \hom {{\target X}_d} \Set {{\target X}_\epsilon}} & \hom {{\target X}_d} \Set {{\target X}_{d''}} & \ni {\target X}_\delta{\target X}_\epsilon \xlongequal{\textstyle {\target {\tilde X}}} {\target X}_{\delta\epsilon}\\ & \mkern{30mu} \Bigg\downarrow \mkern{-30mu} \hom x \Set {{\target X}_{d'}} & \textstyle \hom x \Set {{\target X}_\epsilon} \atop \textstyle \text{(assoc in $\Set$)} & \mkern{30mu} \Bigg\downarrow \mkern{-30mu} \hom x \Set {{\target X}_{d''}} \\ x{\target X}_\delta \in & \hom 1 \Set {{\target X}_{d'}} & \xrightarrow{\textstyle \hom 1 \Set {{\target X}_\epsilon}} & \hom 1 \Set {{\target X}_{d''}} & \ni (x{\target X}_\delta){\target X}_\epsilon \xlongequal{\textstyle\text{assoc}} x({\target X}_\delta{\target X}_\epsilon) \xlongequal{\textstyle {x\target {\tilde X}}} x{\target X}_{\delta\epsilon}\\ & \llap\cong \big\downarrow && \big\downarrow \rlap\cong\\ x\delta \in & \target X_{d'} & \xrightarrow[\textstyle \target X_\epsilon]{} & \target X_{d''} & \ni (x\delta)\epsilon = x(\delta\epsilon)\\ \end{array}\] The left side of the above diagram is ${\hat x}_{d'}$; the right side is ${\hat x}_{d''}$;thus the diagram gives \[\begin{array}{} \delta \in & \hom d \catd {d'} & \xrightarrow{\textstyle \hom d \catd \epsilon} & \hom d \catd {d''} & \ni \delta\epsilon\\ & \llap{{\hat x}_{d'}} \bigg\downarrow & {\hat x}_\epsilon & \bigg\downarrow \rlap{{\hat x}_{d''}}\\ x\delta \in & \target X_{d'} & \xrightarrow[\textstyle \target X_\epsilon]{} & \target X_{d''} & \ni (x\delta)\epsilon = x(\delta\epsilon)\\ \end{array} \taglabel{iaf-ext-nat-1D} \] so the total diagram shows that ${\hat x}_{d'}\,{\target X}_\epsilon \xlongequal{\textstyle {\hat x}_\epsilon} \hom d \catd \epsilon\,{\hat x}_{d''}$,
which gives naturality of $\hat x$ at $\epsilon$.
The above proof amounts to different ways of evaluating the 2-diagram in the 2-category $\CAT$: \[\bbox[20px,border:4px groove black]{\begin{array}{} \cati & \xlongequal{} & \cati\\ \llap{d''}\Bigg\downarrow \mkern{-8mu} \buildrel \textstyle \epsilon \over \Longleftarrow \mkern{-4mu} \Bigg\downarrow \mkern{-10mu}d' \mkern{-8mu} \buildrel \textstyle \delta \over \Longleftarrow \mkern{-8mu} \Bigg\downarrow\rlap{d} & \buildrel \textstyle x \over \Longleftarrow & \Bigg\downarrow\rlap{1}\\ \catd & \target{\xrightarrow[\textstyle X]{}} & \Set \\ \end{array}} \taglabel{iaf-ext-nat-2D} \]
Sublemma. The $\eqref{iaf-bij}$ bijection is natural in its parameters $(\source d \in \catd)$ and $(\target X \in [\catd,\Set])$.
Suppose ($\source{d \buildrel \textstyle\delta \over \rightarrow d'}$ in $\catd$) and ($\target{X \buildrel \textstyle\phi \over \Rightarrow Y}$ in $[\catd,\Set]$).
Then, given $\big(\homst d \catd - \buildrel \textstyle\tau \over \Rightarrow \target X$ in $[\catd,\Set]\big)$,
we have the 2-diagram in $\CAT$
\[\bbox[20px,border:4px groove red]{\begin{array}{}
\cati & \xlongequal{} & \cati\\
\llap{d'}\Bigg\downarrow \mkern{-10mu} \buildrel \textstyle \delta \over \Longleftarrow \mkern{-10mu} \Bigg\downarrow\rlap d & & \Bigg\downarrow\rlap{1}\\
\catd & \begin{smallmatrix}
\xrightarrow[]{\textstyle \homst {\source{d'}} \catd -}\\
\textstyle \Downarrow \rlap{\homst {\source\delta} \catd -}\\
\xrightarrow[\textstyle \homst {\source d} \catd -]{}\\
\textstyle \Downarrow \rlap \tau\\
\target{\xrightarrow[\textstyle X]{}}\\
\target{\textstyle \Downarrow \rlap \phi}\\
\target{\xrightarrow[\textstyle Y]{}}\\
\end{smallmatrix} & \Set \\
\end{array}}\; . \taglabel{iaf-nat-2D}\]
Adding the extraordinary naturality of $1_-$ at $\delta$
to the situation in that 2-diagram
gives the naturality of restriction $\check{()}$ at $\source\delta$, $\target\phi$, and $\tau$:
The naturality requirement on the restriction, $\check{()}$, direction of $\eqref{iaf-bij}$
is that the following diagram in $\Set$ commutes
\[\begin{array}{}
\tau && \check \tau\\
\hom {\homst d \catd -} {[\catd,\Set]} {\target X} & \xrightarrow{\;\textstyle \homst d {\check{()}} X \;} & \target X_d\\
\mkern{46mu} \Bigg\downarrow \mkern{-60mu} \hom {\homst {\source\delta} \catd -} {[\catd,\Set]} {\target \phi} & \homst {\source\delta} {\check{()}} {\target\phi} & \Bigg\downarrow \rlap{\target\phi_{\source\delta}}\\
\hom {\homst {d'} \catd -} {[\catd,\Set]} {\target Y} & \xrightarrow[\; \textstyle \homst {d'} {\check{()}} Y \;]{} & \target Y_{d'}\\
(\homst {\source\delta} \catd -)\tau\target\phi && \big((\homst {\source\delta} \catd -)\tau\target\phi\big)\check{} = \check\tau \target\phi_{\source\delta}
\end{array} \taglabel{iaf-nat-1D}\]
To show that the two legs, when evaluated at a given $\tau \in \hom {\homst d \catd -} {[\catd,\Set]} {\target X}$, agree,
we expand diagram $\eqref{iaf-res-ext-1D}$ a bit,
adding the triangle for the right unit law for $\source\delta$ to its left side
and adding the naturality square for $\target\phi$ at $\source\delta$ to its right side
to get the following commutative diagram in $\Set$:
\[\begin{array}{}
&&\xrightarrow{\displaystyle \check\tau}\\
1 & \xrightarrow{\textstyle \source{1_d}} & \hom d \catd d & \xrightarrow{\textstyle \tau_d} & \target X_d & \xrightarrow{\textstyle \target\phi_d} & \target Y_d\\
\llap{1_{d'}}\bigg\downarrow & \searrow \llap{\raise3pt{\source\delta}} & \mkern{8mu} \bigg\downarrow \mkern{-20mu} \hom d \catd \delta & \tau_{\source\delta} & \mkern{6mu} \bigg\downarrow \mkern{-15mu} \target X_{\source\delta} & \target\phi_{\source\delta} & \mkern{8mu} \bigg\downarrow \mkern{-12mu} \target Y_{\source\delta}\\
\hom {d'} \catd {d'} & \xrightarrow[\textstyle \hom {\source\delta} \catd {d'}]{} & \hom d \catd {d'} & \xrightarrow[\textstyle \tau_{d'}]{} & \target X_{d'} & \xrightarrow[\textstyle \target\phi_{d'}]{} & \target Y_{d'}\\
\end{array} \taglabel{iaf-nat'-1D}\]
where, again, the squares commute by
extraordinary naturality of $1_-$, naturality of $\tau$, and naturality of $\target\phi$, all at $\source\delta$.
The bottom edge is $\big((\homst \delta \catd -)\tau\target\phi\big)_{d'}$,
so the left and bottom edges give $\big((\homst \delta \catd -)\tau\target\phi\big)\check{}$;
the top and right edges give $\check\tau \target\phi_{\source\delta}$.
So $\big((\homst \delta \catd -)\tau\target\phi\big)\check{} \xlongequal{\textstyle \homst \delta {\check{()}} \phi} \check\tau \target\phi_{\source\delta}$, giving the naturality we desire.
Remark:
The above sublemma may be stated as saying the following is a pair of mutually inverse natural transformations in $\CAT$: \[\begin{array}{rcccl} (\hom d \catd -, X) \in & [\catd, \Set]^{\rm op} \times [\catd, \Set] & \xlongequal[]{} & [\catd, \Set]^{\rm op} \times [\catd, \Set] & \ni (\hom d \catd -, X)\\ & \llap{\hom - \catd - \times [\catd, \Set]} \Bigg\uparrow & \llap{\hat{()}}\Bigg\Uparrow \; \Bigg\Downarrow\rlap{\check{()}} & \Bigg\downarrow \rlap{\hom - {[\catd, \Set]} - }\\ &&&& \ni \hom {\hom d \catd -} {[\catd, \Set]} X \\ (d, X) \in & \catd \times [\catd, \Set] & \xrightarrow[\textstyle \rm eval]{} & \Set \\ &&&& \ni X_d \\ \end{array}\]
Work in progress:
