This is a very incomplete start on a more complete document concerning the paper
Street, Ross; Walters, Robert (1978). "Yoneda structures on 2-categories". J. Algebra. 50 (2): 360–379. doi:10.1016/0021-8693(78)90160-6. MR 0463261.
Right now, without giving the full background, I just want to mention (several key diagrams) used to prove (that paper’s Axiom 1) in (the most familiar case, in $\CAT$).
To start, let us recall the basic "iaf/Yoneda lemma" proved in the previous post “The identities-are-free (Yoneda) lemma”.
The basic iaf/Yoneda lemma may be restated 2-categorically as asserting that,
if ($d$ is an admissible object in a category $\catd$),
then the following is a left extension diagram in the 2-category $\CAT$:
\[\begin{smallmatrix}{}
\textstyle\cati \mkern{10mu} & & \buildrel \textstyle 1 \over \longrightarrow & & \mkern{10mu} \textstyle\Set \\
& \llap{\lower3pt\hbox{$d$}}\textstyle\searrow & \raise10pt\hbox{$\textstyle\big\Downarrow\rlap{\textstyle 1_d }$} & \textstyle\nearrow\rlap{\lower3pt\hbox{$\homst d \catd -$}} \\
& & \textstyle\catd \\ \end{smallmatrix}\]
On the other hand, Street and Walters’ Yoneda structure Axiom 1 (YS1),
applied to (the functor $d : \cati \to \catd$),
would assert the existence of a left extension diagram in the 2-category $\CAT$:
\[\begin{smallmatrix}{}
\textstyle\cati \mkern{10mu} & & \xrightarrow[]{\textstyle y\cati} & & \mkern{10mu} \textstyle P\cati\\
& \llap{\lower3pt\hbox{$d$}}\textstyle\searrow & \raise10pt\hbox{$\textstyle\big\Downarrow\rlap{\textstyle \chi^d }$} & \textstyle\nearrow\rlap{\lower3pt\hbox{$\homst d \catd -$}} \\
& & \textstyle\catd \\ \end{smallmatrix}\]
so we see that the basic Yoneda lemma gives YS1 in this special case,
if we define
\[\begin{array}{} P\cati = [\cati^{\rm op}, \Set]\\
y\cati = \homst * \cati -\\
\chi^d = \homst * d -\end{array}\]
and note that $[\cati^{\rm op},\Set] \cong \Set$, $\homst * \cati - \cong 1$ (actually, $\ulcorner 1 \urcorner$), and $\homst * d - \cong 1_d$.
First, they generalize (the functor $d : \cati \to \catd$) (which is merely the name of a single object in $\catd$)
to (functors $f : \source\cata \to \target\catb$ satisfying a smallness condition, which they call admissibility).
Second, they generalize (the ambient environment) from (the 2-category $\CAT$) to (an arbitrary 2-category $\twocatk$).
So Street and Walters postulate a 2-category $\twocatk$,
with a distinguished class of arrows (1-cells), called admissible,
which is closed under precomposition with arbitrary arrows,
making the class an “ideal” under precomposition.
Objects are called admissible when their identity arrow is admissible.
Their Yoneda structure Axiom 1 (YS1) is then:
For every (admissible object $\source A$) and (admissible arrow $f : \source A \to \target B$) in $\twocatk$,
there is a left extension diagram in $\twocatk$:
\[\bbox[20px,border:4px groove red]{\begin{smallmatrix}{}
\textstyle \source A \mkern{10mu} & & \xrightarrow[]{\textstyle y\source A} & & \mkern{10mu} \textstyle P\source A\\
& \llap{\lower3pt\hbox{$f$}}\textstyle\searrow & \raise10pt\hbox{$\textstyle\big\Downarrow\rlap{\textstyle \chi^f }$} & \textstyle\nearrow\rlap{\lower3pt\hbox{$\homst f B -$}} \\
& & \textstyle \target B \\ \end{smallmatrix}} \taglabel{YS1} \]
In this document we want to show that, with suitable definitions,
this axiom is true when (the 2-category $\twocatk$) is $\CAT$.
The admissible arrows are
those functors $f: \source\cata \to \target\catb$ such that $(\forall \source{a\in\cata}, \target{b\in\catb})(\homst {\source a f} {\target\catb} {\target b} \in\Set)$,
i.e., $\source{(\forall a\in\cata)} \target(\source a f$ is an admissible object in $\target{\catb)}$.
The admissible objects in $\CAT$ are then the locally small categories,
those $\catd\in\CAT$ such that $(\forall d,d'\in\catd)\,(\homst d \catd {d'} \in \Set)$,
i.e., every $d\in\catd$ is an admissible object in $\catd$.
Suppose we have two functors in $\CAT$:
| \[\begin{array}{} \source\cata & \buildrel \textstyle f \over \longrightarrow & \target\catb \\ \source a & \mapsto & \source a f\\ \source{\llap\alpha \Big\downarrow} & \mapsto & \target{\Big\downarrow} \rlap{\source\alpha f} \\ \source {a'} & \mapsto & \source{a'} f\\ \end{array}\] | and | \[\begin{array}{} \source{\cata^{\rm op}} \times \target\catb & \buildrel \textstyle X \over \longrightarrow & \Set \\ (\source {a}, \target {b}) & \mapsto & \homst a X b \\ \llap{\Big(\source{\alpha_0 \Big\uparrow}} , \rlap{\target{\Big\downarrow \beta}\Big)} & \mapsto & \Big\downarrow \rlap{\mkern{-29mu}\homst {\alpha_0} X \beta}\\ (\source {a_1}, \target {b'}) & \mapsto & \homst {a_1} X {b'} \\ \end{array}\] |
are also known as bimodules, or profunctors (nlab, Wikipedia), or distributeurs.)
Fix an $\boxed{\source{a\in\cata}}$.
We wish to consider elements $\boxed{\red{x \in {}} \hom {\source a} X {\source a f}}$.
Each such $\red{x \in {}} \hom {\source a} X {\source a f}$ may be considered as a 2-cell of the following form in $\CAT$:
\[\begin{array}{} & \xrightarrow[]{\textstyle 1} \\
\cati & \red{ \Downarrow\rlap x } & \Set \\
& \source{{} \xrightarrow[\textstyle a]{} \cata} \xrightarrow [\textstyle f]{} \target\catb \xrightarrow[\textstyle \homst a X {-'} ]{} \\
\end{array} \]
which is equal to each of the following 2-cells in $\CAT$:
| \[\begin{array}{} & \xrightarrow[]{\textstyle 1} \\ \cati & \red{ \Downarrow\rlap x } & \Set \\ & \source{{} \xrightarrow[\textstyle a]{} \cata} \xrightarrow[\textstyle \hom {\source a} X {\target(\source{?'} \black f\target)}]{} \\ \end{array} \] | and | \[\begin{array}{} & \xrightarrow[]{\textstyle 1} \\ \cati & \red{ \Downarrow\rlap x } & \Set \\ & \target{ {} \xrightarrow[\textstyle \source a \black f]{} \catb } \xrightarrow[\textstyle \hom {\source a} X {-'}]{} \\ \end{array} \] |
- iaf applied to $\cati \source{{} \xrightarrow[\textstyle a]{} \cata} \xrightarrow[\textstyle \hom {\source a} X {\target(\source{?'} \black f\target)}]{} \Set$ gives an ($\source{a'\in\cata}$)-indexed family of functions $\boxed{(\source{\hom a \cata {a'} \xrightarrow[]{\textstyle \hom a \sigma {a'}} {}} \hom {\source a} X {\source{a'}f} )_{\source{a'\in\cata}}}$, natural in $\source{a'\in\cata}$, while
- iaf applied to $\cati \target{{} \xrightarrow[\textstyle \source a \black f]{} \catb} \xrightarrow[\textstyle \homst a X -]{} \Set$ gives a ($\target{b'\in\catb}$)-indexed family of functions $\boxed{(\target{\hom {\source a \black f} \catb {b'} \xrightarrow[]{\textstyle \homst a \tau {b'}} {}} \homst a X {b'} )_{\target{b'\in\catb}}}$, natural in $\target{b'\in\catb}$
(which in fact is two instances of the iaf-res-ext-1D diagram pasted along their common 1-cell $1 \xrightarrow[]{\textstyle \source{\hom a {\check\sigma} {}} = \red x = \target{\homst a {\check\tau} {}}} \hom {\source a} X {{\source a} f} \; $).
\[\begin{array}{} &&&&& 1 \\ &&&& \llap{1_a}\swarrow && \searrow \rlap{1_{af}} \\ && \mkern{-80mu} \source{\llap\alpha \swarrow} & \hom a {\source\cata} a && \llap{\source{\hom a {\check\sigma} {}} = {}} \red{\bigg\downarrow \mkern{-14mu} \boxed x} \rlap{{} = \target{\homst a {\check\tau} {}}} && \hom {af} {\target\catb} {af} & {} \rlap{\mkern{60mu} \target{\searrow \rlap\beta}} \\ && \llap{\source{\hom a \cata \alpha}} \swarrow && \llap{\hom a {\source\sigma} a} \searrow && \swarrow \rlap{\hom a {\target\tau} {af}} && \searrow \rlap{\hom {af} {\target\catb} {\target\beta}} \\ \source{\alpha\in} & \hom a {\source\cata} {a'} && \source{\hom a \sigma \alpha} && \hom a X {af} && \hom a {\target\tau} {\target\beta} && \hom {af} {\target\catb} {\target {b'}} & \target{\ni\beta}\\ && \llap{\source{\boxed{\hom a \sigma {a'}}}} \searrow && \llap{\hom {\source a} X {\source\alpha f}} \swarrow && \searrow \rlap{\homst a X \beta} && \swarrow \rlap{\target{\boxed{\hom {\source a} \tau {b'}}}} \\ &&& \hom {\source a} X {\source{a'}f} &&&& \homst a X {b'} \\ &&& \llap{ \source{(\alpha) \hom a \sigma {a'}} } = \rlap{ (\red x ) \hom {\source a} X {\source\alpha f} } &&&& \llap{ (\red x ) \hom {\source a} X {\target\beta} } = \rlap{ \target{(\beta ) \hom {\source a} \tau {b'}} } \\ \end{array}\]
The following bijections and equalities in $\Set$ are mediated by the equalities under them in $\CAT$:
| $\Set:$ | $\hom {\source{\hom a \cata {?'}}} {\source{[\cata , \black\Set]}} {\hom {\source a} X {\target(\source{?'}f\target)}}$ | $\cong$ | $\source{\big(} \hom {\source a} X {\target(\source{?'} \black f\target)} \source{\big)}_{\source a}$ | $=$ | $\hom {\source a} X {\source a f}$ | $=$ | $\target{\big(} \homst a X - \target{\big)}_{\target( \source a f \target)}$ | $\cong$ | $\hom {\target{\hom {(\source a \black f)} \catb -}} {\target{[\catb , \black\Set]}} {\homst a X -}$ |
|---|---|---|---|---|---|---|---|---|---|
| $\CAT:$ | \[\bbox[20px,border:4px groove black]{\begin{array}{} \cati & \xrightarrow{\textstyle 1} & \Set \\ \source{ \llap a \Big\downarrow } & \source{\Big\Downarrow\rlap{1_a}} & \Big\Vert \\ \source\cata & \twocellctb {\source{\boxed\sigma}} {\source{\hom a \cata -}} {\hom {\source a} X {\target( \source{?'}f \target)}} & \Set \\ \end{array}} \] | $=$ | \[\bbox[20px,border:4px groove black]{\begin{array}{} & \xrightarrow[]{\textstyle 1} \\ \cati & \red{ \Downarrow\rlap x } & \Set \\ & \source{{} \xrightarrow[\textstyle a]{} \cata} \xrightarrow[\textstyle \hom {\source a} X {\target(\source{?'} \black f\target)}]{} \\ \end{array}} \] | $=$ | \[\bbox[20px,border:4px groove black]{\begin{array}{} \cati & \xrightarrow{\textstyle 1} & \Set\\ \source{ \llap{a} \Big\downarrow } & \red{ \Big\Downarrow\rlap x } & \Big\uparrow \rlap{ \homst a X - } \\ \source\cata & \xrightarrow[\textstyle f]{} & \target\catb \\ \end{array}}\] | $=$ | \[\bbox[20px,border:4px groove black]{\begin{array}{} & \xrightarrow[]{\textstyle 1} \\ \cati & \red{ \Downarrow\rlap x } & \Set \\ & \target{ {} \xrightarrow[\textstyle \source a \black f]{} \catb } \xrightarrow[\textstyle \hom {\source a} X -]{} \\ \end{array}} \] | $=$ | \[\bbox[20px,border:4px groove black]{\begin{array}{} \cati & \xrightarrow{\textstyle 1} & \Set \\ \source{\llap a \downarrow} \\ \source\cata & \target{\Big\Downarrow\rlap{1_{\source a \mkern{-1mu} \black f}}} & \Big\Vert \\ \llap f \downarrow \\ \target\catb & \twocellctb {\target{\boxed\tau}} {\target{\hom {\source a \black f} \catb -}} {\homst a X -} & \Set \\ \end{array}} \] |
Now suppose that, (for each $\source{a\in\cata}$), we have (an $\red{\homst a x {} \in {}} \hom {\source a} X {\source a f}$).
The family $\boxed{(\red{\homst a x {} \in {}} \hom {\source a} X {\source a f})_{\source{a \in \cata}}}$ determines as above two biindexed families of functions:
- an ($\source{a\in\cata, a'\in\cata}$)-indexed family of functions $\boxed{(\source{\hom a \cata {a'} \xrightarrow[]{\textstyle \hom a \sigma {a'}} {}} \hom {\source a} X {\source{a'}f} )_{\source{a\in\cata, a'\in\cata}}}$ which, for each fixed $\source{a\in\cata}$, is natural in $\source{a'\in\cata}$, and
- an ($\source{a\in\cata}, \target{b'\in\catb}$)-indexed family of functions $\boxed{(\target{\hom {\source a \black f} \catb {b'} \xrightarrow[]{\textstyle \homst a \tau {b'}} {}} \homst a X {b'} )_{\source{a\in\cata}, \target{b'\in\catb}}}$ which, for each fixed $\source{a\in\cata}$, is natural in $\target{b'\in\catb}$,
Sublemma
The following three naturality conditions on these families are logically equivalent:
- $\source{(\forall a'\in\cata) \Big[ (\hom a \cata {a'} \xrightarrow[]{\textstyle \hom a \sigma {a'}} {}} \hom {\source a} X {\source{a'}f} )_{\source{a\in\cata}}$ is natural in $\source{a\in\cata \Big] }$,
- $\red( 1 \red{{}\xrightarrow[]{\textstyle \homst a x {}} {}} \hom {\source a} X {\source a f} \red)_{\source{a\in\cata}}$ is extraordinarily natural in $\source{a\in\cata}$,
- $\target{(\forall b'\in\catb)} \source{\Big[} \target{(\hom {\source a \black f} \catb {b'} \xrightarrow[]{\textstyle \homst a \tau {b'}} {}} \homst a X {b'} \target)_{\source{a\in\cata}}$ is natural in $\source{a\in\cata \Big] }$.
Thus we have the
Lemma. (YS1, bimodule form)
\[\bbox[20px,border:4px groove red]{ \hom {\source{\hom ? \cata {\source{?'}}}} {\source[ \source{\cata^{\rm op}\times\cata} , \Set \source] } {\hom {\source ?} X {\target(\source{?'} f\target)}} \cong \red\{ \red( 1 \red{{}\xrightarrow[]{\textstyle \homst a x {}} {}} \hom {\source a} X {\source a f} \red)_{\source{a\in\cata}} \;\; \text{extraordinarily natural in $\source{a\in\cata}$} \red\} \cong \hom {{\hom {(\source ? f)} {\target\catb} -}} {\target[ {\source{\cata^{\rm op}}\times\target\catb} , \Set \target] } {\homst ? X -} }\]
Proof of sublemma.
First, here are the 1-diagrams (the commutativity of which) expresses (the naturality conditions) with regard to (an arrow $\source{\alpha_0 : \obja_1 \to \obja}$ in $\source\cata$):
| the naturality of $\hom ? \sigma \objap$ | the extraordinary naturality of $\homst ? x {}$ | the naturality of $\homst ? \tau \objbp$ | ||||
| \[\begin{array}{} \source{ \obja } \\ \source{ \llap{\alpha_0} \bigg\uparrow } \\ \source{ \obja_1 } \\ \end{array}\] | \[\begin{array}{} \source{\hom a \cata {a'}} & \source{\xrightarrow[]{\textstyle \hom a \sigma {a'}}} & \hom {\source a} X {\source{a'}f} \\ \source{ \mkern{12mu} \bigg\downarrow \mkern{-29mu} \hom {\alpha_0} \cata {a'} } & \source{ \hom {\alpha_0} \sigma {a'} } & \mkern{12mu} \bigg\downarrow \mkern{-29mu} \hom {\source{\alpha_0}} X {{\source{a'}f}} \\ \source{ \hom {a_1} \cata {a'} } & \source{ \xrightarrow[\textstyle \hom {a_1} \sigma {a'}]{} } & \hom {\source{a_1}} X {\source{a'}f} \\ \end{array} \] | \[\begin{array}{} 1 & \red{ \xrightarrow[]{\textstyle \hom {\source a} x {}} } & \hom {\source a} X {\source a f} \\ \red{ \llap{\homst {a_1} x {} } \bigg\downarrow } & \homst {\alpha_0} {\red x} {} & \mkern{12mu} \bigg\downarrow \mkern{-29mu} \hom {\source{\alpha_0}} X {\source a f} \\ \hom {\source{a_1}} X {\source{a_1} f} & \xrightarrow[\textstyle \hom {\source{a_1}} X {\source{\alpha_0} f}]{} & \hom {\source{a_1}} X {\source a f} \\ \end{array} \] | \[\begin{array}{} \hom {\source{a}f} {\target\catb} {\target{b'}} & \target{ \xrightarrow[]{\textstyle \hom {\source a} \tau {b'}} } & \homst a X {b'} \\ \mkern{17mu} \target{\bigg\downarrow} \mkern{-35mu} \hom {\source{\alpha_0} f} {\target\catb} {\target{b'}} & \homst {\alpha_0} {\target\tau} {b'} & \mkern{12mu} \bigg\downarrow \mkern{-29mu} \hom {\source{\alpha_0}} X {\target{b'}} \\ \hom {\source{a_1}f} {\target\catb} {\target{b'}} & \target{ \xrightarrow[\textstyle \hom {\source{a_1}} \tau {b'}]{} } & \homst {a_1} X {b'} \\ \end{array} \] | |||
| the right face of the diagram for $\sigma$ below | the common lower left face of both diagrams below | the right face of the diagram for $\tau$ below |
The following diagrams are used to prove the sublemma.
The diagrams are missing the diagonal arrows for the instances of $\source\sigma$ and $\target\tau$,
due to limitations in the TeX/LaTeX/MathJax software which is producing the diagrams,
but if you print out the page containing the diagrams you can easily fill in the diagonals yourself.
(In each diagram there should be six parallel diagonal arrows -- one for $1_1$ and five for the instances of either $\source\sigma$ or $\target\tau$.)
Which is not a bad exercise, by the way.
Or you can just let your imagination fill in the diagonal arrows.
\[\begin{array}{} && \target{\buildrel \textstyle \beta \over \rightarrow} \\ 1 & \xrightarrow[]{\textstyle 1_{\source{a}f}} & \hom {\source{a}f} {\target\catb} {\source{a}f} & \xrightarrow[]{\textstyle \hom {\source{a}f} {\target\catb} {\target\beta}} & \hom {\source{a}f} {\target\catb} {\target{b'}} & \target{\ni \beta} \\ \llap{1_{\source{a_1} f}}\bigg\downarrow & \llap{\lower3pt\hbox{$\source{\alpha_0} f \!\!$}} \searrow & \mkern{17mu} \bigg\downarrow \mkern{-35mu} \hom {\source{\alpha_0} f} {\target\catb} {\source{a}f} & \hom {\source{\alpha_0} f} {\target\catb} {\target\beta} & \mkern{17mu} \bigg\downarrow \mkern{-35mu} \hom {\source{\alpha_0} f} {\target\catb} {\target{b'}} \\ \hom {\source{a_1} f} {\target\catb} {\source{a_1} f} & \xrightarrow[\textstyle \hom {\source{a_1} f} {\target\catb} {\source{\alpha_0} f}]{} & \hom {\source{a_1} f} {\target\catb} {\source{a}f} & \xrightarrow[\textstyle \hom {\source{a_1} f} {\target\catb} {\target\beta}]{} & \hom {\source{a_1} f} {\target\catb} {\target{b'}} \\ & 1_1 & \homst a {\check\tau} {} & \hom {\source a} {\target\tau} {\source a f} & \homst a {\target\tau} \beta & \homst a {\target\tau} {b'} \\ & \homst {a_1} {\check\tau} {} & \homst {\alpha_0} {\check\tau} {} \red? & \hom {\source \alpha_0} {\target\tau} {\source a f} \red? & \homst {\alpha_0} {\target\tau} \beta \red? & \homst {\alpha_0} {\target\tau} {b'} \red? \\ & \hom {\source{a_1}} {\target\tau} {\source{a_1} f} & \hom {\source{a_1}} {\target\tau} {\source{\alpha_0} f} & \hom {\source a_1} {\target\tau} {\source a f} & \homst {a_1} {\target\tau} \beta & \homst {a_1} {\target\tau} {b'} \\ && 1 & \xrightarrow[]{\textstyle \homst a {\red x} {} } & \hom {\source{a}} X {\source{a}f} & \xrightarrow[]{\textstyle \homst a X \beta } & \homst a X {b'} & \ni (\hom {\source a} {\red x} {}) \homst a X \beta = (\target\beta) \homst a {\target\tau} {b'} \\ && \llap{\homst {a_1} {\red x} {}}\bigg\downarrow & \homst {\source{\alpha_0}} {\red x} {} \red? & \mkern{12mu} \bigg\downarrow \mkern{-29mu} \hom {\source{\alpha_0}} X {\source{a} f} & \hom {\source{\alpha_0}} X {\target\beta} & \mkern{12mu} \bigg\downarrow \mkern{-29mu} \hom {\source{\alpha_0}} X {\target{b'}} \\ && \hom {\source{a_1}} X {\source{a_1} f} & \xrightarrow[\textstyle \hom {\source{a_1}} X {\source{\alpha_0} f}]{} & \hom {\source{a_1}} X {\source{a}f} & \xrightarrow[\textstyle \hom {\source{a_1}} X {\target\beta}]{} & \hom {\source{a_1}} X {\target{b'}} \\ \end{array} \taglabel{tau-nat-in-A} \]
Also:
\[\begin{array}{} && \source{\buildrel \textstyle \alpha \over \rightarrow} \\ 1 & \xrightarrow[]{\textstyle 1_{\source{a}}} & \hom {\source{a}} {\source\cata} {\source{a}} & \xrightarrow[]{\textstyle \hom {\source{a}} {\source\cata} {\source\alpha}} & \hom {\source{a}} {\source\cata} {\source {a'}} & \source{\ni \alpha} \\ \llap{1_{\source{a_1}}}\bigg\downarrow & \llap{\lower3pt\hbox{$\source{\alpha_0}\!\!\!\!$}} \searrow & \mkern{12mu} \bigg\downarrow \mkern{-28mu} \hom {\source{\alpha_0} } {\source\cata} {\source{a}} & \hom {\source{\alpha_0} } {\source\cata} {\source\alpha} & \mkern{12mu} \bigg\downarrow \mkern{-28mu} \hom {\source{\alpha_0} } {\source\cata} {\source {a'}} \\ \hom {\source{a_1}} {\source\cata} {\source{a_1}} & \xrightarrow[\textstyle \hom {\source{a_1}} {\source\cata} {\source{\alpha_0}}]{} & \hom {\source{a_1}} {\source\cata} {\source{a}} & \xrightarrow[\textstyle \hom {\source{a_1}} {\source\cata} {\source\alpha}]{} & \hom {\source{a_1}} {\source\cata} {\source {a'}} \\ & 1_1 & \homst a {\check\sigma} {} & \source{\hom a \sigma a} & \homst a {\source\sigma} \alpha & \source{\hom a \sigma {a'}} \\ & \homst {a_1} {\check\sigma} {} & \homst {\alpha_0} {\check\sigma} {} \red? & \source{\hom {\alpha_0} \sigma a} \red? & \source{\hom {\alpha_0} \sigma \alpha} \red? & \source{\hom {\alpha_0} \sigma {a'}} \red? \\ & \source{\hom {a_1} \sigma {a_1}} & \source{\hom {a_1} \sigma {\alpha_0}} & \source{\hom {a_1} \sigma a} & \source{\hom {a_1} \sigma \alpha} & \source{\hom {a_1} \sigma {a'}} \\ && 1 & \xrightarrow[]{\textstyle \homst a {\red x} {} } & \hom {\source{a}} X {\source{a}f} & \xrightarrow[]{\textstyle \hom {\source {a}} X {\source\alpha f}} & \hom {\source{a}} X {\source {a'}f} & \ni (\hom {\source a} {\red x} {}) \hom {\source a} X {\source\alpha f} = (\source\alpha) \hom {\source a} {\source\sigma} {\source{a'}} \\ && \llap{\homst {a_1} {\red x} {}}\bigg\downarrow & \homst {\source{\alpha_0}} {\red x} {} \red? & \mkern{12mu} \bigg\downarrow \mkern{-29mu} \hom {\source{\alpha_0}} X {\source{a}f} & \hom {\source{\alpha_0}} X {\source\alpha f} & \mkern{12mu} \bigg\downarrow \mkern{-29mu} \hom {\source{\alpha_0}} X {\source{a'}f} \\ && \hom {\source{a_1}} X {\source{a_1} f} & \xrightarrow[\textstyle \hom {\source{a_1}} X {\source{\alpha_0} f}]{} & \hom {\source{a_1}} X {\source{a}f} & \xrightarrow[\textstyle \hom {\source{a_1}} X {\source\alpha f}]{} & \hom {\source{a_1}} X {\source{a'} f} \\ \end{array} \taglabel{sigma-nat-in-A} \]
The text of the proof of the above is currently being filled in.
$\target{(\forall b'\in\catb)} \source{\Big[} \target{(\hom {\source a \black f} \catb {b'} \xrightarrow[]{\textstyle \homst a \tau {b'}} {}} \homst a X {b'} \target)_{\source{a\in\cata}}$ is natural in $\source{a\in\cata \Big] }$
iff
$\target{(\forall b'\in\catb)}\source{(\forall \alpha_0 \in \hom {a_1} \cata a)}$ [the right face $\homst {\alpha_0} {\target\tau} {b'}$ of the $\homst {\alpha_0} {\target\tau} \beta$ cube commutes].
Assume the above is true and take $\target{b'} = \source a f$.
Then $\source{(\forall \alpha_0 \in \hom {a_1} \cata a )}$ [the left face $\hom {\source{\alpha_0}} {\target\tau} {\source a f}$ of the $\homst {\alpha_0} {\target\tau} \beta$ cube commutes].
Evaluating at $1_{\source a f}$ and using $\hom {\source{a_1}} {\target\tau} {\source{\alpha_0}f}$ gives (to be filled in).
Work in progress:
No comments:
Post a Comment