The strong Yoneda lemma

Draft:

Kelly, ECT $\S\;$ 2.4 (2.31)

\[ \boxed{ \begin{array} {} && \hom {\hom K \calA -} {[\calA,\calV]} { \rightcat F} \\ && \Vert\kern-.1em\vert \\  && \rightadj{ \displaystyle \int_{\black A} \black{ [ \hom K \calA {\rightcat A}, {\rightcat F_A} ] } } \\ & \leftcat{ \llap{?? \exists!} \nearrow } & \rightadj{\Big\downarrow \rlap{\lambda_{\rightcat A}} } \\ \leftcat X & \rightcat{ \xrightarrow [\textstyle \alpha_A] {\kern3em} }  & [ \hom K \calA {\rightcat A}, {\rightcat F_A} ] \\ & \leftcat{ \llap{\exists! \eta} \searrow  }  & \rightadj{  \Big\uparrow \rlap{ \boxed{ \overline{ \rightcat{\hom {\black K} F A} } \equiv \phi_{\rightcat A} }  }   }  \\  && {\rightcat F}_K  \\  \hline \\  \leftcat X \tensor \hom K \calA {\rightcat A} & \xrightarrow{} &  \rightcat{F_A}  \\ \leftcat X \tensor \hom K \calA {\rightcat K} & \xrightarrow{} &  \rightcat{F_K} & {} \rlap{ \kern-3em \text{the instance } A=K } & \kern4em \\ \\  \hline \hom K \calA {\rightcat A} & \rightcat{  \xrightarrow { \textstyle \overline{\alpha_A} }  } &  [ \leftcat X, {\rightcat F_A} ] & \leftcat X  \\  & \rightcat{  \llap{\hom {\black K} F A} \searrow \rlap{ \leftcat{(1.48)} }  } & \Big\uparrow \rlap{ \kern -1.5em [\leftcat\eta, \rightcat{F_A}] } & \leftcat{ \Big\downarrow \rlap{ \boxed{\exists! \eta} }  }   \\   && [{\rightcat F}_K, \rightcat{F_A}] & {\rightcat F}_K \\ \\  \hline {} \rlap{ \kern-2em \text{instantiating the last triangle at } A=K \text{ gives} } \\ \hline \hom K \calA {\rightcat K} & \rightcat{  \xrightarrow { \textstyle \overline{\alpha_K} }  } &  [ \leftcat X, {\rightcat F_K} ] & \leftcat X  \\  & \rightcat{  \llap{\hom {\black K} F K} \searrow \rlap{ \leftcat{(1.48)} }  } & \Big\uparrow \rlap{ \kern -1.5em [\leftcat\eta, \rightcat{F_K}] } & \leftcat{ \Big\downarrow \rlap{ \boxed{\exists! \eta} }  } & \kern1em  \\ && [{\rightcat F}_K, \rightcat{F_K}] & {\rightcat F}_K  \\ \\  \hline {} \rlap{ \kern-2em \text{precomposing that triangle with } j_K \text{ gives } \eta = 1_K \overline{\alpha_K} }  \\ \end{array} } \]

To recover the weak version of the Yoneda lemma of Section 1.9,, 

take $\leftcat{X=I}$.

$\eta = \overline{\alpha_K} (1_K) $

<hr />

\[ \boxed{ \begin{array} {} \kern2em & \rightcat{\mathbf P} & \xrightarrow { \textstyle \rightcat{\hom q {\mathbf P} -} } & \leftcat{\mathbf V} \\ \hline  & p \\ &&& \nwarrow \rlap{ \hom q {\mathbf P} {p} } \\ & \rightcat{ \llap{ \hom p {\mathbf P} {p'} } \Bigg\downarrow } & \xrightarrow {  \textstyle \hom p { \big( \hom q {\mathbf P} - \big) } {p'}  } & \Big\downarrow & q \\. &&& \swarrow \rlap{ \hom q {\mathbf P} {p'} } \\ & p'  \end{array} } \]

\[ \boxed{ \begin{array} {} q,p \in {} & P \times P & \xrightarrow { \textstyle \text{hom}_{\mathbf P} = {\hom - {\mathbf P} -} } & V & {} \ni \hom q {\mathbf P} p = \overrightarrow{qp} \\   && \llap{ {\hom - P -} = \text{Hom}_P } \searrow & \Big\downarrow \rlap {U = \hom 0 V -}  \\  &&& \cattwo \\ & \theta: & \hom q P p & \cong & \hom 0 V {(\hom q {\mathbf P} p)} \\ && q = p & \iff & 0 = {\hom q {\mathbf P} p}  \\  \end{array} } \tag{tailored version of ECT (1.33)}  \]