Thursday, June 24, 2021

Draft : Comma category notation

First note that, for all $x,y$,  either $x\lt y$ or $y\lt x$ since $h(x,y)$ has to be one of $x,y$.

Suppose $x,y,z$ are distinct elements such that $x\lt y$, $y\lt z$, and $z\lt x$. This last is equivalent to $h(x,z) = z$.  
We write $h(x,z) =??? z$ to indicate this hypothesis is in question.

Then, using the assumption that $h$ is a consistent choice function, we have

\[ \begin{array} {}  x & = & h(x,y) & = & h\big( h(x,y),h(y,z) \big)  \\  &&&& \Vert  \\  &&&&  h(x,y,z)  \\   &&&& \Vert  \\  y & = & h(y,z) & =??? & h\big( h(y),h(x,z) \big)  \\  \end{array} \]

contradicting $x,y$ are distinct.




\[ \leftcat{  \boxed{   \begin{array} {cc|ccccc l|ccccccccc}    \calJ \rlap{\kern.5em \xrightarrow[\kern15em]{\textstyle G} }  &&&  &&  \leftcat{(l\downarrow \calL)}  {} \rlap{  \kern.5em \rightcat{ \xrightarrow[\kern39em]{\textstyle Q = r} }  }   &&&  && &&&  \calL   &&        \\                    \hline     &&&     &&   \llap{\boxed{1}\;} G  &&& \kern1em  & \kern1em   &  \boxed{2}  & G\rightcat Q &&     \\  &&&     &&    &  \rightadj{\nwarrow \rlap\pi}  & \rightadj{\boxed{5}}  &&   & \llap{G\lambda} \nearrow & \smash{ \lower1ex{ \boxed{43=2} } }  &  \rightadj{ \nwarrow \rlap\pi }  & \rightadj{\boxed{3}}     \\     &&&     &&   &&  \rightadj{\big((\black G\rightcat Q)\lim_{\leftcat\calL}\big)}[\overline{G\lambda}]    &&   \leftcat{\llap{\boxed{0}\kern1em}  l} & {} \rlap{\kern-1em \xrightarrow[\textstyle \exists!\overline{G\lambda} \; \boxed{4}]{\kern12em} }  &&&  \rightadj{(\black G\rightcat Q)\lim_{\leftcat\calL}}   \\  &&&    &&   {} \rlap{ \kern3em \text{a single cone} }   &&&& {} \rlap{\kern0em \text{mediating arrow, a morphism of cones} } &&&&   \\                   \hline    &&&    \forall \; \boxed{6} \; k[\kappa]  &  {} \rlap{ \kern-1em \xrightarrow[\kern17em]{\textstyle \forall \mu \; \boxed{7}}  }  &&&  \black G  \rlap{\; \boxed{1}}    \kern1em  &  \kern1em  &  & \boxed{6\rightcat Q} &  k & {} \rlap{ \kern-1em \xrightarrow [\kern12em] {\textstyle \mu\rightcat Q =  \mu \; \boxed{7}} } &&& \black G\rightcat Q  & \boxed{2}      \\  &&&    &    \llap{ \exists! \; \boxed{8'} \; \bar\mu} \searrow  && \rightadj{ \nearrow \rlap{\pi} }   &     &     && \llap{\kappa} \nearrow && \llap{\black G\lambda} \nearrow \rlap{\boxed{2}} && \rightadj{ \nearrow \rlap{\pi} } &   \\   &&&   &&  \rightadj{ \big((\black G\rightcat Q)\lim_{\leftcat\calL}\big) } [\overline{\black G\lambda}]     & \rightadj{\boxed{5}}  &   &&   \llap{\boxed{0}\kern1em}  l & {} \rlap{ \kern-1em \xrightarrow [\textstyle \exists!\overline{\black G\lambda} \; \boxed{4}] {\smash{\kern12em}} } &&& \rightadj{(\black G\rightcat Q)\lim_{\leftcat\calL}}  &  \rightadj{\boxed{3}}  &   \\   \end{array}  }   } \]





\[ \leftcat{ \boxed{ \begin{array} {c|cc|c|cccc|c|cccccc}             \calJ \rlap{ \xrightarrow[\kern12em]{\textstyle \boxed{ \black G = \black G \rightcat Q [\black G \lambda]} } }  & \boxed{ (l\downarrow {\rightadj R}) } \rlap{ \rightcat{ \kern.5em \xrightarrow[ \textstyle \kern4.5em \text{faithful} \kern4.5em ]{\textstyle Q=r} } } & & \rightcat\calR \rlap{ \rightadj{ \kern.5em \xrightarrow[\kern7em]{\textstyle R} } } & & \calL &&  \kern2em &&&&  \CAT   \\       \hline j & X = j\black G = j \big( \black G \rightcat Q [\black G \lambda] \big) = j \black G \rightcat Q [j \black G \lambda] = \rightcat r [\kappa] && \kern2em j\black G\rightcat Q = \rightcat r \kern1em &&& j\black G\rightcat Q\rightadj R = \rightcat r \rightadj R      \\        & &&&& \llap{j \black G \lambda = \kappa} \nearrow &   \\       \llap\iota \Bigg\downarrow & \llap{\iota \black G = {}} \Bigg\downarrow \rlap{ {} = \iota \black G \rightcat Q = \rightcat\rho } && \llap{ \iota \black G \rightcat Q \; } \Bigg\downarrow \rlap{ {} = \rightcat\rho} &  \kern1em l &  {} \rlap{\kern0em \iota \black G = \rightcat\rho}  &  \Bigg\downarrow \rlap{\iota \black G \rightcat Q\rightadj R = \rightcat\rho \rightadj R } & & & &  \boxed{ (l\downarrow {\rightadj R}) }  &  \rightcat{ \kern.5em \xrightarrow[ \textstyle \text{faithful} ]{\textstyle Q=r} } & \rightcat\calR  \\      && && & \llap{j' \black G \lambda = \kappa'} \searrow & \\       j' & X' = j' \black G = j' \big( \black G \rightcat Q [\black G \lambda] \big) = j' \black G \rightcat Q [j' \black G \lambda] = \rightcat{r'} [\kappa'] && j' \black G\rightcat Q = \rightcat{r'} &&& j' \black G\rightcat Q\rightadj R = \rightcat{r'} \rightadj R   \\            \hline              &  \rightadj{   \Bigg\downarrow \rlap{  \kern1em {{\rightcat r} [\kappa]} \mathrel{\rightadj\mapsto} {{(\rightcat r \rightadj R)} [\kappa]} }  }   &&&&&&  &&& \Bigg\downarrow  & \rightadj{ \text{p.b.} } & \rightadj{ \Bigg\downarrow\rlap{R} }   &  \\                 \hline      \calJ \rlap{ \xrightarrow[\kern12em]{\textstyle \boxed{ \black G = \black G \rightcat Q [\black G \lambda]} } }  & \boxed{ (l\downarrow\calL) } \rlap{ \rightcat{ \xrightarrow[ \textstyle \kern10em \text{faithful} \kern6em ]{\textstyle Q=r} } } & & & &\calL &&    \\ \hline      j & X = j\black G = j \big( \black G \rightcat Q [\black G \lambda] \big) = j \black G \rightcat Q [j \black G \lambda] = k[\kappa]  &&&&& j\black G\rightcat Q = k   \\   & &&&& \llap{j \black G \lambda = \kappa} \nearrow & & &  \\   \llap\iota \Bigg\downarrow & \llap{\iota \black G = {} } \Bigg\downarrow \rlap{ {} = \iota \black G \rightcat Q = \mu } & && l &  {} \rlap{\kern0em \iota \black G = \mu}  & \Bigg\downarrow \rlap{\iota \black G \rightcat Q = \mu} & & & & \boxed{ (l\downarrow\calL) } & \rightcat{ \xrightarrow[ \textstyle \text{faithful} ]{\textstyle Q=r} }  &   \leftcat\calL  \\     && && & \llap{j' \black G \lambda = \kappa'} \searrow &    &&&& \llap{!} \downarrow & \Uparrow \rlap\lambda & \Vert \rlap{1_\calL}  \\   j' & X' = j' \black G = j' \big( \black G \rightcat Q [\black G \lambda] \big) = j' \black G \rightcat Q [j' \black G \lambda] = k'[\kappa']  &&&&& j' \black G\rightcat Q = k'   &&&&  \calI  & \xrightarrow[\textstyle l]{}  &  \calL \\     \end{array} } } \]

\[ \leftcat{ \boxed{ \begin{array} {cc|c|ccc|ccccc|c|cc|cccc} \R^2 & \kern2em && \kern2em & \boxed{ (l\downarrow\calL) } \rlap{ \kern.5em \rightcat{ \xrightarrow[ \textstyle \kern2.6em \text{faithful} \kern2.6em ]{\textstyle Q=r} } } & & & & \calL &&9 \kern2em &&11 & \rightcat\calR \rlap{ \xrightarrow[\kern3.5em]{\textstyle \rightadj R } } & \kern0em & \kern0em &\calL &&9 \\ \hline X = \langle X\pi_1,X\pi_2 \rangle = \langle x,y \rangle &&&& \black X = \black X \rightcat Q [\black X \lambda] = k[\kappa] && &&& X\rightcat Q = k &&&& \rightcat r &&&& \rightcat r \rightadj R \\ && && &&& & \llap{X\lambda = \kappa} \nearrow & &&&&& && \llap\kappa \nearrow & \\ && && \Bigg\downarrow \rlap\mu & & \kern2em & l & \mu & \Bigg\downarrow \rlap{\mu\rightcat Q = \mu} &&&& \rightcat{ \llap\rho } \Bigg\downarrow && l & & \rightcat{ \Bigg\downarrow \rlap{\rho \rightadj R} }& \\ & &&&&&& & \llap{X'\lambda = \kappa'} \searrow & &&&& &&& \llap{\kappa'} \searrow & \\ &&&& X' = X' \rightcat Q [X' \lambda] = k' [\kappa'] &&&&& X'\rightcat Q = k' &&&& \rightcat{r'} &&&& \rightcat{r'} \rightadj R \\ \end{array} } } \]

\[ \leftcat{ \boxed{ \begin{array} {cccccc|ccccccc|cccccc} && 1 && \rightadj{\boxed{3}} &    \hskip1em & \hskip1em  &  && 1 && \rightadj{\boxed{3}} &     \\    & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{5}\;\big((GQ)\lim_{\leftcat\calL}\big)[\overline{G\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black G \rightcat Q)\lim_{\leftcat\calL}} } & &   \hskip1em & \hskip1em &      & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{5}\;\big((GQ)\lim_{\leftcat\calL}\big)[\overline{G\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black G \rightcat Q)\lim_{\leftcat\calL}} } & &        \\     \calJ & \xrightarrow[\kern3.5em\boxed{1}\kern3.5em]{\smash{\textstyle G}} & \leftcat{   (l \downarrow \calL)  \rlap{  \lower2.8ex{ \kern-2em \boxed{0} }  }   } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{0}\kern3.55em]{\textstyle Q = r} }  & \calL &   \hskip1em & \hskip1em  & \calJ & \xrightarrow[\kern3.5em\boxed{1}\kern3.5em]{\smash{\textstyle G}} & \leftcat{   (l \downarrow \calL) \rlap{  \lower2.8ex{ \kern-2em \boxed{0} }  }     } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{0}\kern3.5em]{\smash{\textstyle Q = r} }  }  & \calL    \\    {} \rlap{\kern-2em \text{CWM Exercise V.1.1}}  &&  \Bigg\downarrow & \llap{\boxed{0}\;\lambda} \Bigg\Uparrow  & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  &  \hskip1em & \hskip1em &    \Bigg\downarrow & \rightadj{ {} \rlap{ \kern4em \raise3.6ex{\llap{\boxed{3}\;\pi}  \bigg\Uparrow} } } & \rightadj{   \nearrow \rlap{\kern-6.2em \lower1ex{\boxed{3}\;(\black G\rightcat Q)\lim}}   }   & {} \rlap{ \kern-5.4em  \lower4ex{ \bigg\Uparrow \rlap{ \overline{\black G\lambda}\;\boxed{4} } }   } & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  & \kern1em    \\     && 1 & \xrightarrow[\textstyle \boxed{0} \; l]{} & \calL &  \hskip1em & \hskip1em &     1 \rlap{ \kern1em \xrightarrow[\textstyle \boxed{0} \; l]{\kern21em} }  &&&& \calL  \\   \end{array} } } \]





\[ \leftcat{ \boxed{ \begin{array} {cccccc|ccccccc|cccccc} && 1 && \rightadj{\boxed{3}} &    \hskip1em & \hskip1em  &  && 1 && \rightadj{\boxed{3}} &     \\    & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{5}\;\big((GQ)\lim_{\leftcat\calL}\big)[\overline{G\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black G \rightcat Q)\lim_{\leftcat\calL}} } & &   \hskip1em & \hskip1em &      & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{5}\;\big((GQ)\lim_{\leftcat\calL}\big)[\overline{G\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black G \rightcat Q)\lim_{\leftcat\calL}} } & &        \\     \calJ & \xrightarrow[\kern3.5em\boxed{1}\kern3.5em]{\smash{\textstyle G}} & \leftcat{   (l \downarrow \calL)  \rlap{  \lower2.8ex{ \kern-2em \boxed{0} }  }   } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{0}\kern3.55em]{\textstyle Q = r} }  & \calL &   \hskip1em & \hskip1em  & \calJ & \xrightarrow[\kern3.5em\boxed{1}\kern3.5em]{\smash{\textstyle G}} & \leftcat{   (l \downarrow \calL) \rlap{  \lower2.8ex{ \kern-2em \boxed{0} }  }     } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{0}\kern3.5em]{\smash{\textstyle Q = r} }  }  & \calL    \\    {} \rlap{\kern-2em \text{CWM Exercise V.1.1}}  &&  \Bigg\downarrow & \llap{\boxed{0}\;\lambda} \Bigg\Uparrow  & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  &  \hskip1em & \hskip1em &    \Bigg\downarrow & \rightadj{ {} \rlap{ \kern4em \raise3.6ex{\llap{\boxed{3}\;\pi}  \bigg\Uparrow} } } & \rightadj{   \nearrow \rlap{\kern-6.2em \lower1ex{\boxed{3}\;(\black G\rightcat Q)\lim}}   }   & {} \rlap{ \kern-5.4em  \lower4ex{ \bigg\Uparrow \rlap{ \overline{\black G\lambda}\;\boxed{4} } }   } & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  & \kern1em    \\     && 1 & \xrightarrow[\textstyle \boxed{0} \; l]{} & \calL &  \hskip1em & \hskip1em &     1 \rlap{ \kern1em \xrightarrow[\textstyle \boxed{0} \; l]{\kern21em} }  &&&& \calL  \\ \end{array} } } \]


\[ \leftcat{ \boxed{ \begin{array} {cccccc|ccccccc|cccccc}   &&&&  \rightcat y     &&&&&   \\     1 & \xrightarrow[\kern3em]{\textstyle  \boxed{  X = \langle X\pi_1,X\rightcat{\pi_2}\rangle = \langle x,\rightcat y \rangle }  } & \leftcat{ {\mathbf R}^2 \rlap{ \lower2.8ex{ \kern-1.3em \boxed{0} } } } & \rightcat{ \xrightarrow[\kern3.5em\boxed{0}\kern3.55em]{\textstyle \pi_2} } & \mathbf R & \hskip1em & \hskip1em & \calJ & \xrightarrow[\kern3.5em\boxed{1}\kern3.5em]{\smash{\textstyle G}} & \leftcat{ (l \downarrow \calL) \rlap{ \lower2.8ex{ \kern-2em \boxed{0} } } } & \rightcat{ \xrightarrow[\kern3.5em\boxed{0}\kern3.5em]{\smash{\textstyle Q = r} } } & \calL \\ && \llap{\pi_1} \Bigg\downarrow \rlap{\boxed{0}} & & & \hskip1em & \hskip1em & \Bigg\downarrow & \rightadj{ {} \rlap{ \kern4em \raise3.6ex{\llap{\boxed{3}\;\pi} \bigg\Uparrow} } } & \rightadj{ \nearrow \rlap{\kern-6.2em \lower1ex{\boxed{3}\;(\black G\rightcat Q)\lim}} } & {} \rlap{ \kern-5.4em \lower4ex{ \bigg\Uparrow \rlap{ \overline{\black G\lambda}\;\boxed{4} } } } & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} } & \kern1em \\ &   x  & \mathbf R & & & \hskip1em & \hskip1em & 1 \rlap{ \kern1em \xrightarrow[\textstyle \boxed{0} \; l]{\kern21em} } &&&& \calL            \\  \hline   \\   \hline          && 1 && \rightadj{\boxed{3}} &    \hskip1em & \hskip1em  &  && 1 && \rightadj{\boxed{3}} &     \\    & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{5}\;\big((GQ)\lim_{\leftcat\calL}\big)[\overline{G\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black G \rightcat Q)\lim_{\leftcat\calL}} } &   \smash{   \lower3ex {\rightcat k}  }  &   \hskip1em & \hskip1em &      & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{5}\;\big((GQ)\lim_{\leftcat\calL}\big)[\overline{G\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black G \rightcat Q)\lim_{\leftcat\calL}} } & &        \\     \calJ & \xrightarrow[\kern3.5em\boxed{1}\kern3.5em]{\smash{\textstyle \boxed { G =  G\rightcat Q [G\lambda]  =  \rightcat k[\kappa] }}} & \leftcat{   (l \downarrow \calL)  \rlap{  \lower2.8ex{ \kern-2em \boxed{0} }  }   } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{0}\kern3.55em]{\textstyle Q = r} }  & \calL &   \hskip1em & \hskip1em  & \calJ & \xrightarrow[\kern3.5em\boxed{1}\kern3.5em]{\smash{\textstyle G}} & \leftcat{   (l \downarrow \calL) \rlap{  \lower2.8ex{ \kern-2em \boxed{0} }  }     } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{0}\kern3.5em]{\smash{\textstyle Q = r} }  }  & \calL    \\    &   \text{CWM Exercise V.1.1}  & \llap{!} \Bigg\downarrow \rlap{\boxed{0}}     & \llap{\boxed{0}\;\lambda} \Bigg\Uparrow  & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  &  \hskip1em & \hskip1em &    \Bigg\downarrow & \rightadj{ {} \rlap{ \kern4em \raise3.6ex{\llap{\boxed{3}\;\pi}  \bigg\Uparrow} } } & \rightadj{   \nearrow \rlap{\kern-6.2em \lower1ex{\boxed{3}\;(\black G\rightcat Q)\lim}}   }   & {} \rlap{ \kern-5.4em  \lower4ex{ \bigg\Uparrow \rlap{ \overline{\black G\lambda}\;\boxed{4} } }   } & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  & \kern1em    \\        && 1 & \xrightarrow[\textstyle \boxed{0} \; l]{} & \calL &  \hskip1em & \hskip1em &     1 \rlap{ \kern1em \xrightarrow[\textstyle \boxed{0} \; l]{\kern21em} }  &&&& \calL  \\ \end{array} } } \]


<hr />

\[ \leftcat{ \boxed{ \begin{array} {cc|ccc|cccc}  & \kern0em & \kern0em & (l\downarrow\calL) \rlap{ \rightcat{ \xrightarrow[ \textstyle \kern4.5em \text{faithful} \kern4.5em ]{\textstyle Q=r} } } & & & & &\calL &9  \\    \\   \hline  &&& \black X = \black X \rightcat Q [\black X \lambda] = k[\kappa]     &&&&& k   \\    &&& &&&& \llap\kappa \nearrow &    \\       &&&  \Bigg\downarrow \rlap\mu & && l & \mu  & \Bigg\downarrow \rlap\mu & \\ &&&& && & \llap\kappa' \searrow &    \\    &&& X' = X' \rightcat Q [X' \lambda] = k' [\kappa']     &&&&& k'  \\             \\  \hline  \\ \hline  \calJ \rlap{ \xrightarrow[\kern11em]{\textstyle \boxed{ \black G = \black G \rightcat Q [\black G \lambda]} }   } & \kern0em & \kern0em & (l\downarrow\calL) \rlap{ \rightcat{ \xrightarrow[ \textstyle \kern4.5em \text{faithful} \kern4.5em ]{\textstyle Q=r} } } & & & & &\calL &9  \\    \\   \hline j &&& j\black G = j \big( \black G \rightcat Q [\black G \lambda] \big) = j \black G \rightcat Q [j \black G \lambda]     &&&&& j\black G\rightcat Q   \\    &&& &&&& \llap{j \black G \lambda} \nearrow &    \\      \llap\iota \Bigg\downarrow &&&  \llap{\iota \black G = {} }   \Bigg\downarrow \rlap{ {} =   \iota \black G \rightcat Q    } & && l & \iota \black G  & \Bigg\downarrow \rlap{\iota \black G \rightcat Q} & \\ &&&& && & \llap{j' \black G \lambda} \searrow &    \\    j' &&& j' \black G = j' \big( \black G \rightcat Q [\black G \lambda] \big) = j' \black G \rightcat Q [j' \black G \lambda]     &&&&& j' \black G\rightcat Q   \\     \end{array} } } \]




<hr />

\[ \leftcat{ \boxed{ \begin{array} {cc|ccc|cccc}  & \kern0em & \kern0em & (l\downarrow\calL) \rlap{ \rightcat{ \xrightarrow[ \textstyle \kern4.5em \text{faithful} \kern4.5em ]{\textstyle Q=r} } } & & & & &\calL &9  \\    \\   \hline  &&& \black X = \black X \rightcat Q [\black X \lambda] = k[\kappa]     &&&&& k   \\    &&& &&&& \llap\kappa \nearrow &    \\       &&&  \Bigg\downarrow \rlap\mu & && l & \mu  & \Bigg\downarrow \rlap\mu & \\ &&&& && & \llap\kappa' \searrow &    \\    &&& X' = X' \rightcat Q [X' \lambda] = k' [\kappa']     &&&&& k'  \\     \end{array} } } \]



\[ \leftcat{ \boxed{ \begin{array} {cc|ccc|cccc} \calJ \rlap{ \xrightarrow[\kern11em]{\textstyle \boxed{ \black G = \black G \rightcat Q [\black G \lambda]} }   } & \kern0em & \kern0em & (l\downarrow\calL) \rlap{ \rightcat{ \xrightarrow[ \textstyle \kern4.5em \text{faithful} \kern4.5em ]{\textstyle Q=r} } } & & & & &\calL &9  \\    \\   \hline j &&& j\black G = j \big( \black G \rightcat Q [\black G \lambda] \big) = j \black G \rightcat Q [j \black G \lambda]     &&&&& j\black G\rightcat Q   \\    &&& &&&& \llap{j \black G \lambda} \nearrow &    \\      \llap\iota \Bigg\downarrow &&&  \llap{\iota \black G = {} }   \Bigg\downarrow \rlap{ {} =   \iota \black G \rightcat Q    } & && l & \iota \black G  & \Bigg\downarrow \rlap{\iota \black G \rightcat Q} & \\ &&&& && & \llap{j' \black G \lambda} \searrow &    \\    j' &&& j' \black G = j' \big( \black G \rightcat Q [\black G \lambda] \big) = j' \black G \rightcat Q [j' \black G \lambda]     &&&&& j' \black G\rightcat Q   \\     \end{array} } } \]


Naturality at those arrows amounts to showing commutativity of the following diagram in $\SET$:

\[ \boxed{ \begin{array} {}  \kern0em & && [\homst d \catD -, {\rightcat X}]  &&  \kern1em  \\   & &  \llap{ [\homst \delta \catD -, \rightcat\phi] } \swarrow &&  \searrow \rlap{ \check {()} }  \\   & [ \homst {d'} \catD -, \rightcat Y ] &&&&  {\rightcat X}_{\leftcat d}  \\  && \llap{ \check{()} } \searrow  && \swarrow \rlap{ {\rightcat\phi}_{\leftcat\delta} }   \\   & && {\rightcat Y}_{ \leftcat{\delta'} }   \\    \end{array}  }  \]

Wednesday, June 16, 2021

Certain preserved limits give left adjoints

WORK IN PROGRESS!

Here we use the fact that (the cone  $\boxed{    \pi : \leftcat{1_{(l \downarrow \rightadj R)} }\lim \Rightarrow \leftcat{1_{(l \downarrow \rightadj R)} }: \leftcat{(l \downarrow \rightadj R)} \to \leftcat{(l \downarrow \rightadj R)}    }$) is (a natural transformation). 
Hence (the following triangles) commute for all ($\rightcat r \leftcat{[\lambda]}\in \leftcat{(l \downarrow \rightadj R)}$) and ($\rightcat f$ as shown):
\[  \boxed{  \begin{array}  {c|cccccc|cccccc}  \leftcat{1_{(l \downarrow \rightadj R)} } & \kern0em   &  \leftcat{1_{(l \downarrow \rightadj R)} }\lim_{(l \downarrow \rightadj R)} &  {} \rlap{   \kern-1em \xrightarrow[\smash{\kern15em}]{\textstyle \rlap{\pi_{\rightcat r[\lambda]}} }  }   &&&  \rightcat r \leftcat{[\lambda]} & \kern0em   &  \leftcat{1_{(l \downarrow \rightadj R)} }\lim_{(l \downarrow \rightadj R)} &  {} \rlap{   \rightcat{  \kern-1em \xrightarrow[\smash{\kern15em}]{\textstyle f }  }  }   &&&  \rightcat r  \leftcat{[\lambda]}     \\      \llap{\pi} \Big\Uparrow &  &&  \llap{ \pi_{\rightcat{ (\black Q\lim_\calR) } \leftcat{ \big[\overline{\lambda}\big] }}  } \nwarrow  &  \pi_{\pi_{\rightcat r \leftcat{[\lambda]}}}  &  \nearrow \rlap{\pi_{\rightcat r[\lambda]}} &&  &&  \llap{ \pi_{\rightcat{ (\black Q\lim_\calR) } \leftcat{ \big[\overline{\lambda}\big] }}  } \nwarrow  &  \pi_{\rightcat f}  &  \nearrow \rlap{ \pi_{\rightcat r[\lambda]} }  \\    \leftcat{   1_{(l \downarrow \rightadj R)} \lim_{(l \downarrow \rightadj R)  }   }  & & &&  \leftcat{1_{(l \downarrow \rightadj R)} }\lim_{(l \downarrow \rightadj R)}  & & && &&    \leftcat{  1_{(l \downarrow \rightadj R)} \lim_{(l \downarrow \rightadj R)}  }    \\ \end{array}  }  \]

To reiterate, (the two triangles above) commute for all ($\rightcat r \leftcat{[\lambda]}\in \leftcat{(l \downarrow \rightadj R)}$) and ($\rightcat f$ as shown) because ($\rightcat\pi$ is a cone).

Using (naturality of $\pi$ at $\pi_{\rightcat r \leftcat{[\lambda]}}$), i.e. $ \pi_{\pi_{\rightcat r \leftcat{[\lambda]}}}$,  plus 
(the uniqueness clause in the universal property of $\leftcat{1_{(l \downarrow \rightadj R)} }\lim_{(l \downarrow \rightadj R)}$), 
we get that $\pi_{\rightcat{ (\black Q\lim_\calR) } \leftcat{ \big[\overline{\lambda}\big] }} = 1_{  \leftcat{1_{(l \downarrow \rightadj R)} }\lim_{(l \downarrow \rightadj R)}  }$.
This, plus (naturality of $\pi$ at $\rightcat f$), i.e. $\pi_{\rightcat f}$,
gives $\rightcat f = \pi_{\rightcat r[\lambda]}$.

This in turn gives us that 
$\leftcat{1_{(l \downarrow \rightadj R)} }\lim_{(l \downarrow \rightadj R)}$ is 
(an initial object in ${(l \downarrow \rightadj R)}$},
which is equivalent to
$\rightcat{ (Q\lim_\calR) } \leftcat{ \big[\overline{\lambda}\big] }$ being 
(a universal arrow from $\leftcat l$ to $\rightadj\calR$) 
which is equivalent to
$\rightcat{ (Q\lim_\calR) }$ being (a left adjoint $\leftcat  l \leftadj L$ for $\leftcat  l$) with ($\leftcat{ \overline{\lambda} }$ its unit).

<hr />

\[ \boxed{ \begin{array} {c|c|c} \kern2em & \kern2em & \kern2em \\ xx & yy & zz \\ \end{array} } \]

\[ \boxed{ \begin{array} {} && r \\ & \llap{\pi_r} \nearrow & \pi_{\pi_r} & \nwarrow \rlap{\pi_r} \\ \leftcat l\leftadj L & {} \rlap{ \kern-1em \xrightarrow[\pi_{\leftcat l\leftadj L}] {\kern8em} } &&& \leftcat l\leftadj L \\ \end{array} } \]

Saturday, June 5, 2021

The creation of limits in comma categories

DRAFT:
WARNING: There are several different systems that one can come up with
to number the various categories, objects, arrows, and 2-cells we need to introduce and discuss. 
Different numbering systems are in use in different places in the following, 
while I think about which, if any, should be the primary numbering system.


This is a somewhat technical, nitty-gritty, topic, involving some fine details,
but it plays a crucial role in proofs of adjoint functor theorems (see Chapter X, Section 1, of Mac Lane's CWM; also its Chapter V, Section 6, both the Lemma stated there and the exercises to that section), and is worth a close look, where details get filled in, to see what is entailed.
$\calK$
Much of this post is an experiment in presentation, experimenting with different ways of presenting the proof, 
in particular different diagrams that present different aspects, parts, or views of what is going on.

<h3>Comma categories: review and notation</h3>
The notation in the proof gets a bit sticky.
There are both notational and conceptual issues.

Let us introduce this topic by comparing 
(the universal 1-cone $\rightadj{ \langle \pi_{\rightcat 1}, \pi_{\rightcat 2} \rangle }$ of a very familiar categorical product, $\R\times\R \cong \R^2$), to 
(the universal 2-diagrams ($\rightcat Q [\leftcat\lambda]$) for $(l \downarrow \calL)$ and $(l \downarrow \rightadj R)$, the comma categories in question).
(For the 1-universal property of those, see Exercise II.6.4 of CWM. 
For a characterization of those as  weighted limits (cylinders) see Kelly 1989 [EO2CL] (4.2) .)

The diagram at left below, for $\R\times\R \cong \R^2$, is in the 1-category of real vector spaces $\Vect$,
the other diagrams are 2-diagrams in the 2-category $\CAT$.
{Further diagrams are below that top diagram.)

\[ \leftcat{ \boxed{ \begin{array} {ccccc|ccccc|ccccc|ccccc}  &  \leftcat{ \boxed{ \R\times\R \cong \R^2 } \rlap{ \lower2.8ex{ \kern-3.2em \boxed{10} } } } & \rightcat{ \xrightarrow[\kern3.5em\boxed{11}\kern3.55em]{\textstyle \pi_2} } & \R & \hskip.5em & \hskip.5em & \leftcat{ \boxed{ (l \downarrow \calL) }  \rlap{ \lower3ex{ \kern-2.2em \boxed{10} } } } & \rightcat{ \xrightarrow[\kern2em\boxed{11} \; \text{faithful} \kern2em]{\textstyle Q = r} } & \calL   &   \hskip.5em & \hskip.5em & \leftcat{ \boxed{ (l \downarrow \rightadj R) }  \rlap{ \lower3ex{ \kern-2.2em \boxed{10} } } } & \rightcat{ \xrightarrow[\kern1.5em\boxed{11} \; \text{faithful} \kern1.5em]{\textstyle Q = r} } & \rightcat\calR   &   \hskip.5em & \hskip.5em &  \boxed{  ( l \downarrow {\rightadj R})  }  &  \xrightarrow[\kern4em]{\textstyle \text{fiber}}  &  \leftcat{ \boxed{ (\Delta \Downarrow {\rightadj R}) }  }  & \rightcat{ \xrightarrow[\kern4em]{\textstyle !} } & \calI     \\       & \llap{\pi_1} \Bigg\downarrow \rlap{\boxed{11}} & & & \hskip0em & \hskip0em & \llap ! {\Bigg\downarrow} \rlap{\boxed{11}} & \llap{\boxed{11}\;\lambda} \Bigg\Uparrow & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} } & \hskip1em & \hskip0em   & \llap ! {\Bigg\downarrow} \rlap{\boxed{11}} & \llap{\boxed{11}\;\lambda} \Bigg\Uparrow & \Bigg\downarrow \rlap{ \rightadj R \; \boxed{0} } & \hskip1em & \hskip0em   &   \llap{!} {\Bigg\downarrow}  & \rightadj{\text{p.b.}}  & \leftcat{\Bigg\downarrow}  & \Bigg\Uparrow  & \rightadj{  \Bigg\downarrow \rlap{ \ulcorner R \urcorner }  }&       \\       & \R & & & \hskip0em & \hskip0em & \calI & \xrightarrow[\textstyle \boxed{1} \; l]{} & \calL & \hskip0em & \hskip0em   & \calI & \xrightarrow[\textstyle \boxed{1} \; l]{} & \calL & \hskip0em & \hskip0em  &  \calI  &  \xrightarrow[\textstyle l]{}  &  \leftcat\calL & \xrightarrow[\textstyle \Delta]{} & [\rightcat\calR,\leftcat\calL]     \\      \end{array} } } \]

\[ \leftcat{ \boxed{ \begin{array} {cc|c|ccc|ccccc|c|ccc|ccc|cccc}  \R^2   \rlap{  \lower3.2ex{ \kern-1.4em \boxed{10} }  } & \kern0em && \kern0em &  (l\downarrow\calL)  \rlap{  \lower3.2ex{ \kern-2.3em \boxed{10} }  }  \rlap{ \kern.5em \rightcat{ \xrightarrow[ \textstyle \kern4em \boxed{11} \; \text{faithful} \kern4em ]{\textstyle Q=r} } } & & & & &  \calL \rlap{  \lower3.2ex{ \kern-1em \boxed{0} }  }   & \kern1em  &&  \kern0em   & \calJ \rlap{ \xrightarrow[\kern4.7em \boxed{12} \kern4.7em] {\textstyle \boxed{ \black G = \black G \rightcat Q [\black G \lambda]} }  } & \kern0em & \kern0em & (l\downarrow\calL) \rlap{  \lower3.2ex{ \kern-2.3em \boxed{10} }  } \rlap{ \rightcat{ \xrightarrow[ \textstyle \kern3.8em \boxed{11} \; \text{faithful} \kern3.8em ]{\textstyle Q=r} } }  & \kern0em & & & &  \calL \rlap{  \lower3.2ex{ \kern-1em \boxed{0} }  }  &    \\      \\   \hline   X = \langle X\pi_1,X\pi_2 \rangle = \langle x,y \rangle &&&&     \black X = \black X \rightcat Q [\black X \lambda] = k[\kappa]     &&&&&  X\rightcat Q = k   &&&&  j &&& j\black G = j \big( \black G \rightcat Q [\black G \lambda] \big) = j \black G \rightcat Q [j \black G \lambda] &&&&& j\black G\rightcat Q    \\    && && &&& & \llap{X\lambda = \kappa} \nearrow & &&&&& &&&&&& \llap{j \black G \lambda} \nearrow &  \\   &&    &&  \Bigg\downarrow \rlap\mu & & \kern2em   & l & \mu  & \Bigg\downarrow \rlap{\mu\rightcat Q = \mu} &&&& \llap\iota \Bigg\downarrow &&& \llap{\iota \black G = {} } \Bigg\downarrow \rlap{ {} = \iota \black G \rightcat Q } & && l & \iota \black G & \Bigg\downarrow \rlap{\iota \black G \rightcat Q} &  \\  & &&&&&& & \llap{X'\lambda = \kappa'} \searrow & &&&& &&&&& && \llap{j' \black G \lambda} \searrow &   \\     &&&&  X' = X' \rightcat Q [X' \lambda] = k' [\kappa']     &&&&& X'\rightcat Q = k'  &&&&  j' &&& j' \black G = j' \big( \black G \rightcat Q [\black G \lambda] \big) = j' \black G \rightcat Q [j' \black G \lambda] &&&&& j' \black G\rightcat Q    \\     \end{array} } } \]

\[ \leftcat{ \boxed{ \begin{array} {c|cc|c|cccc|c|cccccc} \calJ \rlap{ \xrightarrow[\textstyle \kern2em \boxed{12} \; \text{right lax fiber} \kern2em]{\textstyle \boxed{ \black G = \black G \rightcat Q [\black G \lambda]} } } & \boxed{ (l\downarrow {\rightadj R}) } \rlap{ \lower3.2ex{ \kern-2.5em \boxed{10} } } \rlap{ \rightcat{ \kern.5em \xrightarrow[ \textstyle \kern5.5em \boxed{11} \; \text{faithful} \kern5.5em ]{\textstyle Q=r} } } & & \rightcat\calR \rlap{ \rightadj{ \kern.5em \xrightarrow[\kern8em \boxed{0} \kern8em]{\textstyle R} } } & & \calL && \kern2em &&&& \CAT \\ \hline j & X = j\black G = j \big( \black G \rightcat Q [\black G \lambda] \big) = j \black G \rightcat Q [j \black G \lambda] = \black X\rightcat Q [\black X \lambda] = \rightcat r [\kappa] && \kern2em \black{X} \rightcat Q = j\black G\rightcat Q = \rightcat r \kern1em & \kern7em && \black{X} \rightcat Q \rightadj R = j\black G\rightcat Q\rightadj R = \rightcat r \rightadj R = k \\ & &&&& \llap{\black{X} \lambda = j \black G \lambda = \kappa} \nearrow & \\ \llap\iota \Bigg\downarrow & \llap{\iota \black G = {}} \Bigg\downarrow \rlap{ {} = \iota \black G \rightcat Q = \rightcat\rho } && \llap{ \iota \black G \rightcat Q \; } \Bigg\downarrow \rlap{ {} = \rightcat\rho} & \kern1em l & {} \rlap{\kern0em \iota \black G = \rightcat\rho} & \Bigg\downarrow \rlap{\iota \black G \rightcat Q\rightadj R = \rightcat\rho \rightadj R = \mu} & & & & \boxed{ (l\downarrow {\rightadj R}) } & \rightcat{ \kern.5em \xrightarrow[ \textstyle \boxed{11} \; \text{faithful} ]{\textstyle Q=r} } & \rightcat\calR \\ && && & \llap{\black{X'} \lambda = j' \black G \lambda = \kappa'} \searrow & \\ j' & X' = j' \black G = j' \big( \black G \rightcat Q [\black G \lambda] \big) = j' \black G \rightcat Q [j' \black G \lambda] = \black{X'} \rightcat Q [\black{X'} \lambda] = \rightcat{r'} [\kappa'] && \black{X'} \rightcat Q = j' \black G\rightcat Q = \rightcat{r'} &&& \black{X'} \rightcat Q \rightadj R = j' \black G\rightcat Q\rightadj R = \rightcat{r'} \rightadj R = k' \\ \hline & \rightadj{ \Bigg\downarrow \rlap{ \kern1em {{\rightcat r} [\kappa]} \mathrel{\rightadj\mapsto} {{(\rightcat r \rightadj R)} [\kappa]} } } &&&&&& &&& \Bigg\downarrow & \rightadj{ \text{p.b.} } & \rightadj{ \Bigg\downarrow\rlap{R \; \boxed{0}} } & \kern1em \\ \hline \calJ \rlap{ \xrightarrow[\textstyle \kern2em \boxed{12} \; \text{right lax fiber} \kern2em]{\textstyle \boxed{ \black G = \black G \rightcat Q [\black G \lambda]} } } & \boxed{ (l\downarrow\calL) } \rlap{ \lower3.2ex{ \kern-2.5em \boxed{10} } } \rlap{ \rightcat{ \xrightarrow[ \textstyle \kern13em \boxed{11} \; \text{faithful} \kern13em ]{\textstyle Q=r} } } & & & &\calL && \\ \hline j & X = j\black G = j \big( \black G \rightcat Q [\black G \lambda] \big) = j \black G \rightcat Q [j \black G \lambda] = \black X\rightcat Q [\black X \lambda] = k[\kappa] &&&&& \black{X} \rightcat Q = j\black G\rightcat Q = k \\ & &&&& \llap{\black{X} \lambda = j \black G \lambda = \kappa} \nearrow & & & \\ \llap\iota \Bigg\downarrow & \llap{\iota \black G = {} } \Bigg\downarrow \rlap{ {} = \iota \black G \rightcat Q = \mu } & && l & {} \rlap{\kern0em \iota \black G = \mu} & \Bigg\downarrow \rlap{\iota \black G \rightcat Q = \mu} & & & & \boxed{ (l\downarrow\calL) } & \rightcat{ \xrightarrow[ \textstyle \boxed{11} \; \text{faithful} ]{\textstyle Q=r} } & \leftcat\calL \\ && && & \llap{\black{X'} \lambda = j' \black G \lambda = \kappa'} \searrow & &&&& \llap{\boxed{11} \; !} \downarrow & \llap{ \boxed{11} \; \lambda } \Uparrow & \Vert \rlap{1_\calL \; \boxed{0}} \\ j' & X' = j' \black G = j' \big( \black G \rightcat Q [\black G \lambda] \big) = j' \black G \rightcat Q [j' \black G \lambda] = \black{X'} \rightcat Q [\black{X'} \lambda] = k'[\kappa'] &&&&& \black{X'} \rightcat Q = j' \black G\rightcat Q = k' &&&& \calI & \xrightarrow[\textstyle \boxed{1} \; l]{} & \calL \\ \end{array} } } \]

\[ \leftcat{ \boxed{ \begin{array} {cccccc|ccccccc|cccccc}   &&&&  \rightcat y     &&&&&   \\     1 & \xrightarrow[\kern3em]{\textstyle  \boxed{  X = \langle X\pi_1,X\rightcat{\pi_2}\rangle = \langle x,\rightcat y \rangle }  } & \leftcat{ {\R}^2 \rlap{ \lower2.8ex{ \kern-1.3em \boxed{10} } } } & \rightcat{ \xrightarrow[\kern3.5em\boxed{11}\kern3.55em]{\textstyle \pi_2} } & \R & \hskip1em & \hskip1em &  &  &  &  &  \\   && \llap{\pi_1} \Bigg\downarrow \rlap{\boxed{11}} & & & \hskip1em & \hskip1em &  &  & &  &  & \kern1em       \\ &   x  & \R & & & \hskip1em & \hskip1em &      &&&&   \\                          \hline                   && 1 && \rightadj{\boxed{3}} &    \hskip1em & \hskip1em  &  && 1 && \rightadj{\boxed{3}} &     \\    & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{5}\;\big((X\pi_2)\lim_{\leftcat\R}\big)[\overline{X\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black X \rightcat{\pi_2})\lim_{\leftcat\R}} } &   &   \hskip1em & \hskip1em &      & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{5}\;\big((X\pi_2)\lim_{\leftcat\R}\big)[\overline{X\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black X \rightcat \pi_2)\lim_{\leftcat\R}} } & &        \\     &&&&  \rightcat y     &&&&&   \\     (\leftcat a, \rightcat b )   & \xrightarrow[\kern3em]{\textstyle  \boxed{  X = \langle X\pi_1,X\rightcat{\pi_2}\rangle = \langle x,\rightcat y \rangle }  } & \leftcat{ {\mathbf R}^2 \rlap{ \lower2.8ex{ \kern-1.3em \boxed{10} } } } & \rightcat{ \xrightarrow[\kern3.5em\boxed{11}\kern3.55em]{\textstyle \pi_2} } & \mathbf R & \hskip1em & \hskip1em & \calJ & \xrightarrow[\kern3.5em\boxed{1}\kern3.5em]{\smash{\textstyle G}} & \leftcat{ (l \downarrow \calL) \rlap{ \lower2.8ex{ \kern-2em \boxed{10} } } } & \rightcat{ \xrightarrow[\kern3.5em\boxed{11}\kern3.5em]{\smash{\textstyle Q = r} } } & \calL \\ && \llap{\pi_1} \Bigg\downarrow \rlap{\boxed{11}} & & & \hskip1em & \hskip1em & \Bigg\downarrow & \rightadj{ {} \rlap{ \kern4em \raise3.6ex{\llap{ \boxed{21}\;\pi_{\black G \rightcat Q} } \bigg\Uparrow} } } & \rightadj{   \nearrow \rlap{  \kern-6.2em \lower1ex{ \boxed{20}\;(\black G\rightcat Q)\leftcat{\lim_\calL} }  }    } & {} \rlap{ \kern-5.4em \lower4ex{ \bigg\Uparrow \rlap{ \overline{\black G\lambda}\;\boxed{32} } } } & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} } & \kern1em \\ &   x  & \mathbf R & & & \hskip1em & \hskip1em & 1 \rlap{ \kern1em \xrightarrow[\textstyle \boxed{1} \; l]{\kern21em} } &&&& \calL   \\          \hline   \\         && 1 && \rightadj{\boxed{20}} &    \hskip1em & \hskip1em  &  && 1 && \rightadj{\boxed{20}} &     \\    & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{22}\;\big((GQ)\lim_{\leftcat\calL}\big)[\overline{G\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black G \rightcat Q)\lim_{\leftcat\calL}} } &   \smash{   \lower3ex {\rightcat k}  }  &   \hskip1em & \hskip1em &      & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{22}\;\big((GQ)\lim_{\leftcat\calL}\big)[\overline{G\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black G \rightcat Q)\lim_{\leftcat\calL}} } & &        \\     \calJ & \xrightarrow [\kern3.5em\boxed{12}\kern3.5em]{\smash{\textstyle \boxed { G =  G\rightcat Q [G\lambda]  =  \rightcat k[\kappa] }}} & \leftcat{   (l \downarrow \calL)  \rlap{  \lower2.8ex{ \kern-2em \boxed{10} }  }   } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{11}\kern3.5em]{\textstyle Q = r} }  & \calL &   \hskip1em & \hskip1em  & \calJ & \xrightarrow[\kern3.5em\boxed{12}\kern3.5em]{\smash{\textstyle G}} & \leftcat{   (l \downarrow \calL) \rlap{  \lower2.8ex{ \kern-2em \boxed{10} }  }     } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{11}\kern3.5em]{\smash{\textstyle Q = r} }  }  & \calL    \\    &   \text{CWM Exercise V.1.1}  & \llap{!} \Bigg\downarrow \rlap{\boxed{11}}     & \llap{\boxed{11}\;\lambda} \Bigg\Uparrow  & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  &  \hskip1em & \hskip1em &    \Bigg\downarrow & \rightadj{    {} \rlap{   \kern4em \raise3.6ex{  \llap{ \boxed{21} \; \pi_{\black G\rightcat Q} } \bigg\Uparrow  }   }    } & \rightadj{   \nearrow \rlap{\kern-6.2em \lower1ex{\boxed{20}\;(\black G\rightcat Q)\lim_{\leftcat\calL}}}   }   & {} \rlap{ \kern-5.4em  \lower4ex{ \bigg\Uparrow \rlap{ \overline{\black G\lambda}\;\boxed{32} } }   } & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  & \kern1em    \\        && 1 & \xrightarrow[\textstyle \boxed{1} \; l]{} & \calL &  \hskip1em & \hskip1em &     1 \rlap{ \kern1em \xrightarrow[\textstyle \boxed{1} \; l]{\kern21em} }  &&&& \calL  \\          \hline   \\   \hline        &&&&  \rightcat k  &&&&&  \\      \calI & \xrightarrow [\kern3.5em\boxed{1}\kern3.5em]{\smash{\textstyle \boxed { X =  X\rightcat Q [X\lambda]  =  \rightcat k[\kappa] }}} & \leftcat{   (l \downarrow \calL)  \rlap{  \lower2.8ex{ \kern-2em \boxed{0} }  }   } &  \rightcat{ \xrightarrow [\kern3.5em\boxed{0}\kern3.55em]{\textstyle Q = r} }  & \calL &   \hskip1em & \hskip1em  & \calJ & \xrightarrow[\kern3.5em\boxed{1}\kern3.5em]{\smash{\textstyle G}} & \leftcat{   (l \downarrow \calL) \rlap{  \lower2.8ex{ \kern-2em \boxed{0} }  }     } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{0}\kern3.5em]{\smash{\textstyle Q = r} }  }  & \calL    \\    & & \llap{!} \Bigg\downarrow \rlap{\boxed{0}}     & \llap{\boxed{0}\;\lambda} \Bigg\Uparrow  & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  &  \hskip1em & \hskip1em &    \Bigg\downarrow & \rightadj{ {} \rlap{ \kern4em \raise3.6ex{\llap{\boxed{3} \; \pi_{\black G\rightcat Q}}  \bigg\Uparrow} } } & \rightadj{   \nearrow \rlap{\kern-6.2em \lower1ex{\boxed{3}\;(\black G\rightcat Q)\lim}}   }   & {} \rlap{ \kern-5.4em  \lower4ex{ \bigg\Uparrow \rlap{ \overline{\black G\lambda}\;\boxed{4} } }   } & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  & \kern1em    \\        && 1 & \xrightarrow[\textstyle \boxed{0} \; l]{} & \calL &  \hskip1em & \hskip1em &     1 \rlap{ \kern1em \xrightarrow[\textstyle \boxed{0} \; l]{\kern21em} }  &&&& \calL  \\           \hline   \\         && 1 && \rightcat{\boxed{20}} &    \hskip1em & \hskip1em  &  && 1 && \rightcat{\boxed{20}} &     \\    & \llap{!} \nearrow & \red{     \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{22} \; \rightcat{ \big( (\leftcat G  Q)\lim_\calR \big) } \leftcat{ [\overline{G\lambda}] } } }  } & \rightcat{ \searrow \rlap{ (\leftcat G  Q)\lim_\calR }     } &   \smash{   \lower3ex {\rightcat s}  }  &   \hskip1em & \hskip1em &      & \llap{!} \nearrow & \red{     \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{22} \; \rightcat{ \big( (\leftcat G  Q)\lim_\calR \big) } \leftcat{ [\overline{G\lambda}] } } }  } & \rightcat{ \searrow \rlap{ (\leftcat G  Q)\lim_\calR }     } & &        \\     \calJ & \xrightarrow[\kern3.5em\boxed{12}\kern3.5em]{\smash{\textstyle \boxed { G =  G\rightcat Q \leftcat{[G\lambda]}  =  \rightcat s \leftcat{[\kappa]} }}} & \leftcat{   (l \downarrow \rightadj R)  \rlap{  \lower2.8ex{ \kern-2em \boxed{10} }  }   } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{11}\kern3.55em]{\textstyle Q = r} }  & \rightcat\calR &   \hskip1em & \hskip1em  & \calJ & \xrightarrow[\kern3.5em\boxed{12}\kern3.5em]{\smash{\textstyle G}} & \leftcat{   (l \downarrow \rightadj R) \rlap{  \lower2.8ex{ \kern-2em \boxed{10} }  }     } &  \rightcat{ \xrightarrow [\kern3.5em\boxed{11}\kern3.5em]{\smash{\textstyle Q = r} }  }  &  \rightcat\calR   \\    &   \text{CWM Lemma V.6}  & \llap{!} \Bigg\downarrow \rlap{\boxed{11}}     & \llap{\boxed{11}\;\lambda} \Bigg\Uparrow  & \rightadj{     \Bigg\downarrow \rlap{ R \; \boxed{0} }     }  &  \hskip1em & \hskip1em &    \Bigg\downarrow & \rightcat{ {} \rlap{ \kern4em \raise3.6ex{\llap{\boxed{21} \; \pi_{\black G\rightcat Q} }  \bigg\Uparrow} } } & \leftadj{   \nearrow \rlap{  \kern-6.2em \lower1ex{ \boxed{20}\;(\black G\rightcat Q)\lim_{\rightcat\calR} }  }   }   & \leftadj{      {} \rlap{ \kern-5.4em  \lower4ex{ \bigg\Uparrow \rlap{ \leftcat{ \overline{\black G\leftcat\lambda} } \; \boxed{32} } }   }     }   &   \rightadj{     \Bigg\downarrow \rlap{ R \; \boxed{0} }     }  & \kern1em    \\        && 1 & \xrightarrow[\textstyle \boxed{1} \; l]{} & \calL &  \hskip1em & \hskip1em &     1 \rlap{ \kern1em \xrightarrow[\textstyle \boxed{1} \; l]{\kern21em} }  &&&& \calL  \\ \end{array} } } \]

To understand those categories, 
a necessary starting point is to see what the objects and arrows in each look like 
in relation to
the objects and arrows in their constituent categories. 
To that end, consider the above diagrams: 

<hr />

(Repitious repeat, to be edited :-)
Before wading into (the existence proof) for (a limit) in (a comma category), 
it is useful to review the definitions of (the objects and arrows in comma categories), 
and (their relations) to (those in the related categories).
(This is material in Section II.6, Comma Categories, of CWM, adopted with notation tailored to 
(a putative right adjoint functor $\rightadj{ \boxed{0} \; R : \rightcat\calR \to \leftcat\calL }$).)

To that end, consider the above (rather large display).
This display accomplishes several things.
First, it shows (objects and arrows in several different categories and how they relate to each other).
Second, it shows how (objects in comma categories) can be broken into (their components) ($X \mapsto X\rightcat Q, X\leftcat\lambda$), 
and conversely how (compatible entities) can be combined into (an object in a comma category) ($k, \kappa \mapsto k[\kappa]$),
and, moreover, this not just for (individual objects), but also for (functors into comma categories) (variable objects).

<hr />

Suppose we have a path, a function of time, in $\R^2$
Such a path could be denoted as a single variable, say a single letter like $X$, 
or in terms of its coordinates, say $\langle x_1,x_2 \rangle$, or $\langle x,y \rangle$, 
or we could introduce explicit coordinate functions on ${\mathbf R}^2$, say $\pi_1$ and $\pi_2$ 
and view the coordinates as composites $X\pi_1$ and $X\pi_2$, 
which can be combined to give $X$ by: $\boxed{  X = \langle X\pi_1,X\pi_2 \rangle }$.
(I.e., do we show the coordinates of $X$, or merely $X$ as a single entity?)
The same choices arise for functors into comma categories.
($\leftcat{  (l\downarrow\calL) }$) has its "coordinate functions"
($\rightcat Q : \leftcat{  (l\downarrow\calL) } \to \calL$) and ($   \leftcat{  \lambda : {!l} \Rightarrow \rightcat Q :  {(l\downarrow\calL)} \to \calL  }   $).
Thus below I speak about (a functor $G : \calJ \to {(l\downarrow\calL)} $), and its "coordinates" $G\rightcat Q$ and $G\leftcat\lambda$, 
which can be put back together to get $G$ by: $\boxed{  G = G\rightcat Q \leftcat{ [\black G\lambda] }  }$, 
which acts as follows on ($\iota : j \to j'$ in $\calJ$):

\[ \leftcat{ \boxed{ \begin{array} {cc|ccc|cccc} \calJ \rlap{ \xrightarrow[\kern11em]{\textstyle \boxed{ \black G = \black G \rightcat Q [\black G \lambda]} }   } & \kern0em & \kern0em & (l\downarrow\calL) \rlap{ \rightcat{ \xrightarrow[ \textstyle \kern4.5em \text{faithful} \kern4.5em ]{\textstyle Q=r} } } & & & & &\calL &9  \\    \\   \hline j &&& j\black G = j \big( \black G \rightcat Q [\black G \lambda] \big) = j \black G \rightcat Q [j \black G \lambda]     &&&&& j\black G\rightcat Q   \\    &&& &&&& \llap{j \black G \lambda} \nearrow &    \\      \llap\iota \Bigg\downarrow &&&  \llap{\iota \black G = {} }   \Bigg\downarrow \rlap{ {} =   \iota \black G \rightcat Q    } & && l & \iota \black G  & \Bigg\downarrow \rlap{\iota \black G \rightcat Q} & \\ &&&& && & \llap{j' \black G \lambda} \searrow &    \\    j' &&& j' \black G = j' \big( \black G \rightcat Q [\black G \lambda] \big) = j' \black G \rightcat Q [j' \black G \lambda]     &&&&& j' \black G\rightcat Q   \\     \end{array} } } \]

<hr />

In the simplest situation (CWM Exercise V.1.1), 
we start with (a single category $\leftcat{ \boxed{0} \; \calL }$) and (an object $\leftcat{ \boxed{1} \; l \in \calL }$).
We can then form (the comma category $\leftcat{ \boxed{\boxed{10}\;(l\downarrow \calL)} }$)
with its universal 2-diagram in the 2-category $\CAT$,
one leg of which is the (canonical faithful, but not full, forgetful functor 
$\rightcat{  \boxed{\leftcat{(l\downarrow \calL)} \xrightarrow[\kern1em\boxed{11}\kern1em]{\textstyle Q = r} \leftcat\calL : \leftcat{k[\kappa : l \to k] \mathrel{\rightcat\mapsto} k}}  }$).
(The boxed numbers are used in some diagrams below.)

Suppose now we have 
(a functor $\boxed{ \boxed{12} \; G : \calJ \to \leftcat{(l\downarrow \calL)} }$) such that 
(the composite $\boxed{ 12; \rightcat{11} } \; \black G\rightcat Q$) has
(a limit cone $\rightadj{    \boxed{\textstyle \boxed{21}\; \pi_{\black G \rightcat Q} : \boxed{20} \; (\black G\rightcat Q)\lim_{\leftcat\calL} \Rightarrow \black G\rightcat Q}    }$ in $\leftcat\calL$).

\[ \leftcat{ \boxed{ \begin{array} {cccccc|ccccccc|cccccc} && 1 && \rightadj{\boxed{20}} &    \hskip1em & \hskip1em  &  && 1 && \rightadj{\boxed{20}} &     \\    & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{22} \; \big((GQ)\lim_{\leftcat\calL}\big)[\overline{G\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black G \rightcat Q)\lim_{\leftcat\calL}} } & &   \hskip1em & \hskip1em &      & \llap{!} \nearrow & \red{  \Bigg\downarrow \rlap{ \kern-5em \boxed{\textstyle \boxed{22}\;\big((GQ)\lim_{\leftcat\calL}\big)[\overline{G\lambda}]} }  } & \rightadj{ \searrow \rlap{(\black G \rightcat Q)\lim_{\leftcat\calL}} } & &        \\     \calJ & \xrightarrow [\kern3.5em \boxed{12} \kern3.5em] {\smash{\textstyle G}} & \leftcat{   (l \downarrow \calL)  \rlap{  \lower2.8ex{ \kern-2em \boxed{10} }  }   } &  \rightcat{ \xrightarrow [\kern3.5em\boxed{11}\kern3.55em]{\textstyle Q = r} }  & \calL &   \hskip1em & \hskip1em  & \calJ & \xrightarrow[\kern3.5em\boxed{12}\kern3.5em]{\smash{\textstyle G}} & \leftcat{   (l \downarrow \calL) \rlap{  \lower2.8ex{ \kern-2em \boxed{10} }  }     } &  \rightcat{ \xrightarrow[\kern3.5em\boxed{11}\kern3.5em]{\smash{\textstyle Q = r} }  }  & \calL    \\    {} \rlap{\kern-2em \text{CWM Exercise V.1.1}}  &&  \Bigg\downarrow & \llap{\boxed{11}\;\lambda} \Bigg\Uparrow  & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  &  \hskip1em & \hskip1em &    \Bigg\downarrow & \rightadj{ {} \rlap{ \kern4em \raise3.6ex{\llap{ \boxed{21} \; \pi_{\black G \rightcat Q} }  \bigg\Uparrow} } } & \rightadj{   \nearrow \rlap{  \kern-6.2em \lower1ex{ \boxed{20}\;(\black G\rightcat Q)\lim_{\leftcat\calL} }  }   }   &  {} \rlap{ \kern-5.4em  \lower4ex{ \bigg\Uparrow \rlap{ \overline{\black G\lambda}\;\boxed{32} } }   }    & \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }  & \kern1em    \\     && 1 & \xrightarrow[\textstyle \boxed{1} \; l]{} & \calL &  \hskip1em & \hskip1em &     1 \rlap{ \kern1em \xrightarrow[\textstyle \boxed{1} \; l]{\kern25em} }  &&&& \calL  \\ \end{array} } } \]

See (the external 2-diagrams in $\CAT$ above), also (the internal diagrams in two functor categories) in (the first row below).
Ignore for the moment (the second row).
 
\[ \leftcat{  \boxed{   \begin{array} {cccc l|ccccccccc}    &&    [ \calJ, \leftcat{(l\downarrow \calL)} ]  {} \rlap{  \kern.5em \rightcat{ \xrightarrow[\kern37em]{\textstyle [ \leftcat\calJ, (Q=r) ] } }  }   &&&  && &&&  [ \calJ, \calL ]   &&        \\                    \hline     &&   \llap{\boxed{1 | 12}\;} G  && & \kern1em  & \kern1em   &&  \llap{  \boxed{2 | 12;\rightcat{11}} \kern1em }   G\rightcat Q &&     \\     &&    &  \rightadj{  \nwarrow \rlap{ \pi_{\black G} \; \boxed{5 | 121} }  }  &  &&   & \llap{G\lambda} \nearrow & \smash{   \lower1ex{  \boxed{ \scriptstyle \text{defn } \overline{G\lambda} }  }   }  &  \rightadj{  \nwarrow \rlap{ \pi_{\black G \rightcat Q} \; \boxed{3 | 21} }  }     \\       &&   &&  \rightadj{\big((\black G\rightcat Q)\lim_{\leftcat\calL}\big)}[ \overline{G\lambda} ] \; \boxed{5 | 132}  &&   \leftcat{\llap{\boxed{0}\kern1em}  l} & {} \rlap{\kern-1em \xrightarrow[ \textstyle \boxed{ \exists!\overline{G\lambda} \; \boxed{4 | 32} } ]{\kern12em} }  &&&  \rightadj{  (\black G\rightcat Q)\lim_{\leftcat\calL} \; \boxed{3 | 20}  }   \\   &&   {} \rlap{ \kern3em \text{a single $\calJ$-cone in $(l\downarrow \calL)$} }   &&&& {} \rlap{\kern0em \text{mediating arrow, a morphism of $\calJ$-cones in $\calL$} } &&&&   \\                   \hline        \forall \; \boxed{6} \; k[\kappa]  &  {} \rlap{ \kern-1em \xrightarrow[\kern17em]{\textstyle \forall \mu \; \boxed{7}}  }  &&&  \black G  \rlap{\; \boxed{1}}    \kern1em  &  \kern1em  &  & \boxed{6\rightcat Q} &  k & {} \rlap{ \kern-1em \xrightarrow [\kern12em] {\textstyle \mu\rightcat Q =  \mu \; \boxed{7}} } &&& \black G\rightcat Q  & \boxed{2}      \\     &    \llap{ \exists! \; \boxed{8'} \; \bar\mu} \searrow  && \rightadj{  \nearrow \rlap{ \pi_{\black G} \; \boxed{5 | 121} }  }   &     &     && \llap{\kappa} \nearrow && \llap{\black G\lambda} \nearrow \rlap{\boxed{2 | 12;11}} && \rightadj{  \nearrow \rlap{ \pi_{\black G \rightcat Q \;  \boxed{3 | 21}} }  } &   \\   &&  \rightadj{ \big((\black G\rightcat Q)\lim_{\leftcat\calL}\big) } [\overline{\black G\lambda}]     & \rightadj{\boxed{5 | 120}}  &   &&   \llap{\boxed{0}\kern1em}  l & {} \rlap{ \kern-1em \xrightarrow [\textstyle \exists!\overline{\black G\lambda} \; \boxed{4 | 32}] {\smash{\kern12em}} } &&& \rightadj{(\black G\rightcat Q)\lim_{\leftcat\calL}}  &  \rightadj{\boxed{3 | 20}}  &   \\   \end{array}  }   } \]
Then ($\boxed{2}\; G\leftcat\lambda$ is a cone over $\boxed{2}\; G\rightcat Q$), 
($\rightadj{ \boxed{3} \; \pi_{\black G \black Q} }$ is a universal cone over $\boxed{2}\; G\rightcat Q$), 
so there is a unique (mediating arrow $\leftcat{   \boxed{  \boxed{4} \; \overline{{\black G}\lambda}  }   }$) such that $\leftcat{    \boxed{   {  {\overline{\black G\lambda}} \cdot {  \rightadj{ \pi_{\black G \rightcat Q} }  } = {\black G\lambda}   }    }       }$.
Note that ($\rightadj{ \boxed{5}\; \big((\black G\rightcat Q)\lim_{\leftcat\calL}\big)\leftcat{[\overline{\black G\lambda}]} }$ is an object in the comma category $\leftcat{\boxed{0}\; (l\downarrow \calL)}$), and 
**** (the universal cone $\rightadj{\boxed{3} \; \pi_{\black G \rightcat Q} : (\black G\rightcat Q)\lim_{\leftcat\calL} \Rightarrow \black G\rightcat Q}$ in $\leftcat\calL$) 
may also be viewed as 
(a cone $\rightadj{  \boxed{\textstyle \boxed{5}\; \pi_{\black G} : \big((\black G\rightcat Q)\lim_{\leftcat\calL}\big)[\overline{\black G\lambda}] \Rightarrow G}  }$ in $\leftcat{(l\downarrow \calL)}$) ****.

To show ($\rightcat{\boxed{0}\; Q}$ created a limit) we must show 
(the above lift ${\rightadj\pi}_{\rightcat G}$) is (unique as a lift) and (universal as a cone).

For (uniqueness as a lift)
suppose (a cone $\rho : k[\kappa] \Rightarrow G$ in $\leftcat{(l\downarrow \calL)}$) 
is (a lift through $\rightcat Q$) of (the cone $\rightadj{\pi_{\black G \rightcat Q} : (\black G\rightcat Q)\lim_{\leftcat\calL} \Rightarrow \black G\rightcat Q}$ in $\calL$). 
\[ \leftcat{ \boxed{ \begin{array} {cccc|cccccc} {} \rlap{ \kern2em (l \downarrow \calL) \kern.5em \rightcat{ \xrightarrow[\kern24em]{\textstyle Q = r} } } &&&& & && \calL \\ \hline G &&& \kern1em & \kern1em & && G\rightcat Q && \\ & \nwarrow \rlap\rho && \text{a single cone in } \leftcat{(l\downarrow \calL)} && & \llap{G\lambda} \nearrow && \nwarrow \rlap{ \rho\rightcat Q = \rightadj{ \pi_{\black G \rightcat Q} } } & \\ && k[\kappa] &&& \leftcat l & {} \rlap{\kern-1em \xrightarrow[\textstyle \kappa]{\kern9em} } &&& (k[\kappa])\rightcat Q = \rightadj{ (\black G\rightcat Q)\lim_{\leftcat\calL} } \\ &&&&& {} \rlap{\kern0em \text{a morphism of cones in } \leftcat\calL} &&&& \\ \end{array} } } \]
Then $k \xlongequal{ \text{ defn. of } \rightcat Q \, } (k[\kappa])\rightcat Q \xlongequal{ \text{ lift } } \rightadj{  (\black G\rightcat Q)\lim_{\leftcat\calL}  }$
and $\rho = \rho\rightcat Q = \rightadj\pi_{\black G \rightcat Q}$
so $\Big(  \rho : k[\kappa] \Rightarrow G  \Big)$ equals $\rightadj{ \Big( \pi_{\black G} : \big((\black G\rightcat Q)\lim_{\leftcat\calL}\big)[\kappa] \Rightarrow G  \Big)  }$  as (cones in $\leftcat{(l\downarrow \calL)}$).

The only variable yet to be determined is $\kappa$.
But, like $\overline{G\lambda}$,
($\kappa$ is a morphism of cones from $G\lambda$ to $\pi_{\black G \rightcat Q}$), 
and (the uniqueness clause of the universal property of the latter) gives 
$\kappa = \overline{G\lambda}$.



Our job now is to show 
(the cone  $\rightadj{    \boxed{   \textstyle   \boxed{5} \; \pi_{\black G} : \leftcat{   \big((\black G\rightcat Q)\lim_{\leftcat\calL}\big)\Big[\overline{\black G\lambda}\Big]   }  \Rightarrow  \black G   }    }$)
is (a universal cone to $G$ in $\leftcat{(l\downarrow \calL)}$), thus 
$\red{   \boxed{  \textstyle \leftcat{ \big((\black G\rightcat Q) \lim_{\leftcat\calL}\big) \Big[\overline{\black G\lambda}\Big] } = \black G\lim_{ \leftcat{(l\downarrow \calL)} }  }   }$.
(Consult the internal diagrams below; 
numbers in boxes refer to entities in the categories $\leftcat\calL$ and $\leftcat{(l\downarrow \calL)}$.)

\[ \leftcat{ \boxed{ \begin{array} {ccc|c  rcccccl}   \kern1em && \kern-10em &  \kern1em  &&& &&  \llap{ \boxed{1 | 12} \; } \black G &&   \\  &  \leftcat{ \llap{ \boxed{10} \; } (l\downarrow \calL)  }  &&&    && && & \rightadj{ \nwarrow \rlap{\pi_{\black G} \; \boxed{5 | 121}} }  &  \kern4em  \text{(a single cone) in } \leftcat{(l\downarrow \calL)}  \\  &  \smash{   \lower2ex{  \rightcat{ \llap{ \boxed{11} \; Q } \Bigg\downarrow }  }   } &&&     &&&   && & \rightadj{ \big((\black G\rightcat Q) \lim_{\leftcat\calL}\big) } \Big[\overline{\black G\lambda}\Big]  \rightadj{  {} = \black G \lim_{ \leftcat{(l\downarrow \calL)}   } \; \boxed{5 | 120}    }   \\         \hline          &&&& && &&  \llap{ \boxed{2 | 12;11} \; } G\rightcat Q &&   \\     &&&&   && &  \leftcat{  \llap{\boxed{2 | 12;11 , 31} \; G\lambda} \nearrow  }  && \rightadj{ \nwarrow \rlap{\pi_{\black G \black Q} \; \boxed{3 | 21}} } &  \kern4em \rightadj{ \text{(a single, universal, cone) in } \leftcat\calL }   \\    &  \leftcat{  \llap{ \boxed{0} \; } \calL  }   &&&    && \leftcat{  \boxed{0 | 1 , 30} \; l  }   & {} \rlap{\kern-1em \xrightarrow[\textstyle \llap{\boxed{4 | 32} \;} \exists!\overline{G\lambda}] {\kern19em} } &&& \rightadj{  (\black G\rightcat Q)\lim_{\leftcat\calL} \rlap{ \; \boxed{3 | 20} }  }     \\     &&&&& {} \rlap{    \kern0em \text{definition of $\leftcat{\overline{\black G\lambda}}$ makes it (a morphism of cones in  $\leftcat\calL$) : $\leftcat{  \overline{\black G\lambda} : \black G \lambda \to \rightadj{ \pi_{\black G \rightcat Q} }  }$  }     }  &&&&&       \\ \hline \\ \hline       &&&&&  {} \rlap{   \text{($\mu : k[\kappa] \Rightarrow G$ an arbitrary cone) in } \leftcat{(l\downarrow \calL)} \text{ to the base } G  }  \\    &&&& &  & \forall \; \boxed{6} \; k[\kappa] & {} \rlap{ \kern-1em \xrightarrow[\kern18em] {\textstyle \forall\mu \kern1em \boxed{7}} } &&& \black G \rlap{\; \boxed{1 | 12}} \\ &  \leftcat{  \llap{ \boxed{10} \; } (l\downarrow \calL)  } &&& && & \llap{\boxed{8'} \kern1em \exists!\bar\mu} \searrow && \rightadj{ \nearrow \rlap{ \pi_{\black G} \; \boxed{5 | 121} } } &   \kern4em  \text{(a single cone) in } \leftcat{(l\downarrow \calL)}   \\   & \smash{   \lower2ex{   \rightcat{  \llap{ \boxed{11} \; Q} \Bigg\downarrow  }   }    }      &&& && && \rightadj{ \big((\black G\rightcat Q)\lim_{\leftcat\calL}\big) } \Big[\overline{\black G\lambda}\Big]  \rlap{  \; \rightadj{ \boxed{5 | 120} }  }  &&   \\             \hline              &&&  {} \rlap{   \text{(the $\rightcat Q$-image of (the above cone $\mu : k[\kappa] \Rightarrow  G$)) in $(l\downarrow \leftcat\calL)$ is (a cone $\mu\rightcat Q = \mu : k \Rightarrow G\rightcat Q$) in } \leftcat\calL,    }  \\     &&&  {} \rlap{  \text{thus there exists a unique mediating arrow $\boxed{   \textstyle \boxed{8}\; \bar\mu : k \to \rightadj{ (\black G\rightcat Q)\lim_{\leftcat\calL} }    }$ (not shown) in $\calL$}  }   \\     &&& {} \rlap{   \text{such that $\boxed{8}\; \bar\mu : \mu\rightcat Q \to {\rightadj\pi}_{\black G\rightcat Q}$  is a morphism of cones in $\leftcat\calL$}   }       \\  &&&&   & \boxed{6 \rightcat Q} & k & {} \rlap{ \kern-2em \xrightarrow [\kern20em] {\textstyle \mu \rightcat Q = \mu \kern1em \boxed{7 \rightcat Q}} } &&& \black G\rightcat Q \rlap{  \;  \boxed{ 2 | 12;\rightcat{11} }  }     \\    &  \llap{ \boxed{0} \; } \calL   &&&  & \llap{\kappa} \nearrow \rlap{   \kern-.5em { \text{$\leftcat\mu$ is} \atop \text{a cone in $\leftcat{(l\downarrow\calL)}$} }   }   && {} \rlap{ \kern0em \black G\lambda \nearrow \kern0em \boxed{2} \kern0em { \text{$\overline{\black G\leftcat\lambda}$ is an arrow} \atop \text{between cones in } \calL }   } && \rightadj{  \nearrow \rlap{ \pi_{\black G \rightcat Q} \; \boxed{3 | 21} }  } &  \kern4em  \rightadj{ \text{(a single, universal, cone) in } \leftcat\calL }    \\      &&& \kern0em &  \llap{ \boxed{0} \; } l & {} \rlap{ \kern-1em \xrightarrow [\textstyle \exists!\overline{\black G\lambda} \rlap{\; \boxed{4 | 32}}] {\kern15em} } &&& \rightadj{   (\black G\rightcat Q)\lim_{\leftcat\calL} \rlap{ \; \boxed{3 | 20} }   } && \\   \end{array} } } \]

To that end, let ($\leftcat{\boxed{6} \; k[\kappa]}$ be an object in $\leftcat{(l\downarrow \calL)}$), 
and ($\leftcat{\boxed{7}\; \mu : k[\kappa] \Rightarrow G}$ be a cone in $\leftcat{(l\downarrow \calL)}$).
Then ($\boxed{7 \rightcat Q}\; \mu \rightcat Q = \leftcat{\mu :  k \Rightarrow \black G\rightcat Q}$ is a cone in $\leftcat\calL$), 
so there is a unique (mediating arrow $\leftcat{   \boxed{  \textstyle  \boxed{8}\; \bar\mu : k \to  \rightadj{ (\black G\rightcat Q)\lim_{\leftcat\calL} }  }   }$) 
(not shown in the diagram) such that ($\leftcat{ \bar\mu : \mu \to \rightadj\pi }$ is a morphism of cones in $\leftcat\calL$). 
It remains to show ($\leftcat{ \bar\mu : k \to \rightadj{(\black G\rightcat Q)\lim_{\leftcat\calL}} }$ in $\leftcat\calL$) 
is (an arrow $\leftcat{ \bar\mu : k[\kappa] \to \rightadj{\big((\black G\rightcat Q)\lim_{\leftcat\calL}\big)} \leftcat{\Big[\overline{\black G\lambda}\Big]} }$ in $\leftcat{(l\downarrow \calL)}$).
 Since $\leftcat{ \kappa\bar\mu \rightadj\pi = \kappa\mu = \black G\lambda = \overline{\black G\lambda}\rightadj\pi }$, 
the uniqueness clause in the universal property of $\rightadj\pi$ gives $\leftcat{ \kappa\bar\mu = \overline{\black G\lambda}}$, 
so $\leftcat{ \bar\mu : \mu \to \rightadj\pi}$ is an arrow in $\leftcat{ (l\downarrow \calL) }$
and $\leftcat{ \boxed{8'} \; \bar\mu : \mu \to \rightadj\pi }$ is a morphism of cones in $\leftcat{(l\downarrow \calL)}$ (see the diagram).
Further $\leftcat{ \bar\mu : k[\kappa] \to \rightadj{\big((\black G\rightcat Q)\lim_{\leftcat\calL}\big)}\leftcat{[\overline{\black G\lambda}]} }$ in $\leftcat{(l\downarrow \calL)}$ 
is the unique arrow in $\leftcat{(l\downarrow \calL)}$ such that $\leftcat{\bar\mu} \rightadj\pi = \rightcat\mu$.
Thus $\rightadj{    \pi : \big((\black G \rightcat Q)\lim_{\leftcat\calL}\big) \leftcat{  \big[ \overline{\black G \lambda} \big) ]   } \Rightarrow \black G    }$ is a universal cone in $\leftcat{(l\downarrow \calL)}$.

In those circumstances $\leftcat{ G : \calJ \to (l\downarrow \calL) }$ 
has a limit $\rightadj{\pi : \big((\black G \rightcat Q)\lim_{\leftcat\calL}\big)\leftcat{  [ \overline{\black G \lambda} ]  } \Rightarrow \black G}$  in $\leftcat{(l\downarrow \calL)}$ 
which is preserved by the canonical forgetful functor $\leftcat{(l\downarrow \calL) \to \calL}$.

The above diagrams were internal to respectively $\leftcat\calL$ and $\leftcat{(l\downarrow \calL)}$.
There is an external diagram (in $\CAT$) that is useful in showing relations between the limits:
\[ \leftcat{ \begin{array} {} && 1 \\ & \llap{!} \nearrow & \red{ \Bigg\downarrow \rlap{ \kern-4em \boxed{\textstyle \big((GQ)\lim_{\leftcat\calL}\big)  \big[\bar\lambda\big]} } } &  \searrow \rlap{ (G\rightcat Q)\lim_{\leftcat\calL} }  \\      \calJ & \xrightarrow[\textstyle G]{\kern4em} & \boxed{(l \downarrow \calL)} &  \rightcat{ \xrightarrow[\textstyle Q = r]{\kern4em} }  & \calL  \\    \big\Vert  &&&&  \big\Vert   \\    \calJ &  {} \rlap{ \kern-2em \xrightarrow[\textstyle G\rightcat Q]{\kern17em} } &&& \calL\end{array}  }  \]




<hr />





For the adjoint functor theorems we need a two-category, or "relative," version of the above.
(The boxed numbers below are used in both the text and the diagrams.
They give a sense of the order in which various constructions are made.)
Thus we start with a functor $\rightadj{ \boxed{ {\leftcat\calL} \leftarrow {\rightcat\calR} : R \; \boxed{0} }  }$ 
from ($\rightcat{ \boxed{0} \calR} $, the "right category") (that is my terminology; I do not know how common that terminology is) 
to ($\leftcat{ \boxed{0} \calL }$, the "left category").
Given $\rightadj R$ and (an object $\leftcat{ \boxed{0|1} \; l \in \calL }$ in the left category $\leftcat\calL$),
we consider (the comma category $\leftcat{   \boxed{ \boxed{0|10} \; (l \downarrow {\rightadj R})}   }$) 
and its relations (in the 2-category $\CAT$) to several other entities:

\[   \leftcat{       \boxed{     \begin{array} {cccccc|cc}      &&  1  & \rightcat{ \boxed{3 | 20} }  & & \kern2em & \kern2em  &   &&  1  & \rightcat{ \boxed{3 | 20} } &   \kern2em    \\    &  \llap{!} \nearrow  &  \red{    \Bigg\downarrow \rlap{   \kern-2.5em \boxed{  \textstyle \leftcat G\lim_{ \leftcat{(l \downarrow {\rightadj R})} }  }   }    }   &  \rightcat{ \searrow \rlap{(\leftcat G Q)\lim_\calR} }  & &     &      &     &  \llap{!} \nearrow  &  \red{    \Bigg\downarrow \rlap{   \kern-2.5em \boxed{  \textstyle \leftcat G\lim_{ \leftcat{(l \downarrow {\rightadj R})} }  }   }    }   &  \rightcat{ \searrow \rlap{(\leftcat G Q)\lim_\calR} }  &     \\      \calJ  &  \xrightarrow[\kern1em \boxed{1 | 12} \kern1em]{\textstyle G}  &  \boxed{(l \downarrow {\rightadj R})} \rlap{  \lower3ex{ \kern-2.6em \boxed{0 | 10} }  }   &  \rightcat{ \xrightarrow[\kern1em \boxed{0 | 11} \kern1em]{\textstyle Q = r} }  &  \rightcat\calR    &     &      & \calJ  &  \xrightarrow[\kern1em \boxed{1 | 12} \kern1em]{\textstyle G}  &  \boxed{ (l \downarrow {\rightadj R}) } \rlap{  \lower3ex{ \kern-2.6em \boxed{0 | 10} }  }   &  \rightcat{ \xrightarrow[\kern1em \boxed{0 | 11} \kern1em]{\textstyle Q = r} }   &  \rightcat\calR    &     \\       &&   \Bigg\downarrow   & \llap{ \boxed{0 | 11} \;  \lambda }  \Bigg\Uparrow &  \rightadj{\Bigg\downarrow \rlap{ R \;  \boxed{0} }  } &   {} \rlap{\kern1em \cong}   &      &    {} \rlap{ \kern-2em { \textstyle\text{CWM} \atop \textstyle\text{Exercise V.6.3} }  }    &&   \Bigg\downarrow   &  \rightadj{  \llap{ \boxed{0 | 10} \; } \text{p.b.}  }   &  \rightadj{\Bigg\downarrow  \rlap{ R \;  \boxed{0} } }     \\   &&  1  & \xrightarrow[\smash{\textstyle \boxed{0 | 1} \; l}]{}   &  \calL   &       &       &   &&  \leftcat{(l \downarrow \calL)}  &  \rightcat{ \xrightarrow{} } &  \calL   \\    {} \rlap{\kern1em \text{CWM Lemma V.6, Exercise V.6.1} } &&&&&&&     {} \rlap{ \kern-2em { \textstyle\text{CWM} \atop \textstyle\text{Exercise V.1.1} }  }  &&  \Bigg\downarrow   &  \llap{ \boxed{0 | 11} \; \lambda } \Bigg\Uparrow &  \Bigg\Vert \rlap{ 1_\calL \; \boxed{0} }      \\   &&&&&&&&& 1  &  \xrightarrow[\textstyle \boxed{0 | 1} \; l]{}  &  \calL   \\  \end{array}     }       }    \]

Whereas the diagram above was (an external diagram, in $\CAT$), 
the diagrams below are (internal to the three categories).

\[ \leftcat{ \boxed{ \begin{array} {cccccc c|cccccc c|cccccc} &&& (l\downarrow \rightadj R) \; \boxed{10} \rlap{ \kern.5em \rightcat{ \xrightarrow[\kern28em]{\textstyle Q = r \; \boxed{11}} } } &&&&& &&  \rightcat{ \calR \; \boxed{0} } \rlap{  \kern.5em \rightadj{ \xrightarrow[\kern35em]{\textstyle R \; \boxed{0}} }  } &&&&&&&&&   \calL \; \boxed{0}    \\        \hline      & \forall \; \boxed{6 | 130} \; \rightcat r \leftcat{[\kappa]} & \rightcat{ {} \rlap{ \kern-1em \xrightarrow[ \textstyle \kern3em \text{a cone in } \leftcat{(l\downarrow \rightadj R)} \kern3em ]{\textstyle \forall \rho \; \boxed{7 | 131}} } } &&&   G\;\boxed{1 | 12}  & \kern1em & \kern1em & \boxed{6 \rightcat Q | 30}\;\rightcat{r} & \rightcat{   {} \rlap{  \kern-1em \xrightarrow[ \textstyle \kern2.5em \text{a cone in } \calR \kern2.5em ]{    \textstyle \rho Q = \rho\;\boxed{7Q | 31} }  }   } &&& G \rightcat{ Q \; \boxed{2} } & \kern1em & \kern1em &&&  \llap{ \boxed{6 \rightcat Q \rightadj R | 30 \rightadj R} \; } {\rightcat r}{\rightadj R} &  \rightcat{  {} \rlap{ \kern-3em \xrightarrow [\kern19em] {\textstyle \rho Q \rightadj R = \rho \rightadj R \; \boxed{7 \rightcat Q  \rightadj R | 31\rightadj R} } }  } &&&  G \rightcat{Q} {\rightadj R} \; \boxed{2\rightadj R}  & 8      \\          && \rightcat{ \llap{\exists! \; \boxed{8' | 132} \; \bar\rho} \searrow } && \rightcat{  \nearrow \rlap{ \pi_{\black G} \; \boxed{5 | 121} }  } & &&& & \rightcat{ \llap{\exists! \; \boxed{8 | 32} \; \bar\rho} \searrow } && \rightcat{  \nearrow \rlap{ \pi_{\black G\rightcat Q} \; \boxed{3 | 21} }  } &&&&    &     \llap{ \boxed{6\lambda} \; \kappa } \nearrow   &  \kern-1em { \text{$\rightcat\rho$ is a} \atop \text{cone in $\leftcat{ (l\downarrow{\rightadj R}) }$}  }  \kern1em   & \llap{\black G\lambda} \nearrow \rlap{ \boxed{2} } & { \text{$\overline{\black G\leftcat\lambda}$ is an arrow} \atop \text{between cones in $\leftcat\calL$} }   &   \rightadj{  \nearrow \rlap{ \pi_{\black G\rightcat Q} R  \; \boxed{\rightcat 3 R | 21 R} }  }  && \kern1em \rightadj{ \text{(a single, universal, cone) in } \leftcat\calL }      \\     &&& \rightcat{\big((\black G Q)\lim_\calR\big)}[\overline{\black G\lambda}] \rlap{  \; \rightadj{ \boxed{5 | 120} }  }  &&  && &&&    \rightcat{(\black G Q)\lim_\calR} \rlap{ \rightcat{\; \boxed{3 | 20} }  }  &&&&& l & {} \rlap{ \kern-1em \xrightarrow [ \textstyle \exists!\overline{\black G\lambda} \; \boxed{4 | 22} ] {\kern14em} } &&& \rightadj{ \big(\rightcat{(\black G Q)\lim_\calR}\big) R } \rlap{  \; \boxed{ \rightcat 3 \rightadj R | \rightcat{20} \rightadj R }  }    \\   \end{array} } } \] 

The following combines (an external diagram) with (four internal diagrams) in (one large display). 
The created limits are colored $\red{\text{red}}$.
\[   \boxed{   \begin{array} {c|ccccc|ccccccc|ccccc}  1&  \forall \; \boxed{6 | 130} \; {\rightcat r} \leftcat{[\kappa]} & {} \rightcat{  \rlap{ \kern-2em \xrightarrow[\kern26em]{\textstyle \forall\rho \; \boxed{7 | 131}} }  }   &&&  G = \rightcat{ (\black G Q) } \leftcat{ [{\black G} \lambda] } \; \boxed{1 | 12}  &  \kern0em  & &  &&  &&   && & \rightcat{\boxed{6Q | 30}} & \rightcat r & \rightcat{  {} \rlap{ \kern-1em \xrightarrow [\kern26em] { \textstyle \rho\rightcat Q \; \boxed{7Q | 31}} }  }   &&& \black G\rightcat Q \rlap{\; \rightcat{\boxed{2}}}  & \kern2em    \\           2&  & \leftcat{  \llap{ \exists! \; \boxed{8' | 132} \; \bar\rho} \searrow  }    &    &  \rightadj{  \nearrow \rlap{\pi_{\black G} \; \rightcat{\boxed{3' | 121}} }  }   &&&   \rightcat{ {} \rlap{   \xrightarrow[\textstyle \kern8em \boxed{0 | 11} \kern8em]{\textstyle Q = r} }   }    &  &&  &&  && & & &  \rightcat{ \llap{ \boxed{8 | 32} \; \exists!\overline{\rho Q} } \searrow  }   &   &   \rightcat{ \nearrow \rlap{\pi_{\black G\rightcat Q} \; \boxed{3 | 21} } } &    \\         3&   &&     \smash{ \raise7ex{    \red{ \boxed{  \textstyle \text{limit in } \leftcat{ (l \downarrow {\rightadj R}) } \over {  \textstyle {\black G}\lim_{ \leftcat{ (l \downarrow {\rightadj R}) }  }   =    \atop \textstyle \rightcat{ \big    ((\black G Q)\lim_\calR\big) } \leftcat{ \Big[\overline{\black G \lambda}\Big] }  }   }    }     }      }     & \rightadj{ \boxed{5 | 120} }  &&&&  &&&&     & & & &&&   \smash{     \raise4ex{  \rightcat{  \boxed{ \textstyle \text{limit in } \calR  \over \textstyle (\black G\rightcat Q)\lim_\calR = \leftcat l\leftadj L  }   }    }     }    &  \rightcat{\boxed{3 | 20}}  &       \\    \hline   4&   &&   \leftcat{ (l \downarrow {\rightadj R}) }   &   &&&  \calJ  &  \xrightarrow[\smash{\textstyle \kern1em \boxed{1 | 12} \kern1em}]{\textstyle G}  &  \leftcat{ (l \downarrow {\rightadj R}) } \rlap{   \smash{  \lower3ex{ \kern-2.5em \boxed{0 | 10} }  }   }  & \rightcat{ \xrightarrow[\textstyle \kern1em \boxed{0 | 11} \kern1em]{\textstyle Q = r} } & \rightcat\calR    & & & & &&&   \rightcat\calR  &&       \\      5&   &&  \Bigg\downarrow  &&&&   &&  \leftcat{ \llap ! \Bigg\downarrow }  &  \leftcat{ \llap{\boxed{0 | 11} \; \lambda} {\Bigg\Uparrow} }  &  \rightadj{  \Bigg\downarrow \rlap{ R \; \boxed{0} }  }  &&&&&&&    \rightadj{  \Bigg\downarrow \rlap{ R \; \boxed{0} }  }    \\   6&  && \leftcat{ (l \downarrow \calL) }   &&&& && 1 & \leftcat{ \xrightarrow[\textstyle \boxed{0 | 1} \; l]{} } & \leftcat\calL && & && &&  \leftcat\calL   &  \\   \hline   7&   \forall \; \boxed{6' | 130'} \; \leftcat{  ({\rightcat r}{\rightadj R}) [\kappa]  } & {} \rightcat{  \rlap{ \kern-1em \xrightarrow[\kern27em]{\textstyle \forall\rho \; \boxed{7 | 131} }  }  }   &&&  \leftcat{    (\black G\rightcat Q\rightadj R) [{\black G} \lambda] \rlap{\; \boxed{2 | 11}}    }  & &&& &&&&&& \leftcat{  \boxed{ \rightcat{6Q}\rightadj{R} | \rightcat{30}\rightadj{R} }  } & \rightcat r\rightadj R & {} \rlap{   \kern-1em \xrightarrow [\kern25em] {  \textstyle \rightcat{\rho Q}\rightadj R \; \boxed{ \rightcat{7Q}\rightadj R | \rightcat{31}\rightadj R }  }   }   &&& \black G\rightcat Q\rightadj R \rlap{\; \leftcat{\boxed{2 \rightadj{R}}}}     \\       8&      & \leftcat{   \llap{  \exists! \; \boxed{ {8'\rightadj R | 32 \rightadj R} } \; {\bar\rho}'  } \searrow   }   &&  \rightadj{    \nearrow  \rlap{    {\rightcat\pi}_{\black G\rightcat Q} \rightadj R \; \leftcat{  \boxed{ {\rightcat 3 \rightadj R | \rightcat{21} \rightadj R} }  }   }    }    &&&  \rightcat{ {} \rlap{   \xrightarrow [\textstyle \kern8em \boxed{0 | 11} \kern8em] {\textstyle Q = r} }   } & && && && & \leftcat{ \llap{\boxed{6\lambda} \; \kappa} \nearrow } & \leftcat{ {} \rlap{ \kern0em \black G\lambda \nearrow \kern0em \boxed{2 | \black G 11} } } &&& \rightcat{    \nearrow \rlap{   \rightcat{ \pi_{\black G Q} }  \rightadj{R} \; \leftcat{ \boxed{ \rightcat{3}\rightadj{R} | \rightcat{21}\rightadj R }  }   }    } &   \\    9&         && \smash{ \raise2ex{    \red{ \boxed{  \textstyle \text{limit in } \leftcat{ (l \downarrow \calL) } \over { \textstyle \leftcat{   \Big( \rightcat{\big((\black G Q)\lim_\calR\big)} {\rightadj R} \Big)  } \leftcat{\Big[\overline{\black G \lambda}\Big]} }   }    }     }      }        & \rightadj{ \boxed{5' | 120'} }  &&&& && && \kern1em & \kern1em & \leftcat{ \llap{\boxed{0 | 1}\;} l } & \leftcat{ {} \rlap{ \kern-1em \xrightarrow [ \textstyle \exists!\overline{\black G\lambda} \kern1em \boxed{4 | 32} ] {\kern9em} } } &&&  \smash{     \raise0ex{  \leftcat{  \boxed{ \textstyle \text{limit in } \calL  \over \textstyle  \rightcat{  \big((\black G\rightcat Q)\lim_\calR\big) \rightadj R  } = \leftcat l\leftadj L\rightadj R}   }    }     }   & \leftcat{  \boxed{ \rightcat 3\rightadj R | \rightcat{20}\rightadj R }  }  &  \\   \end{array}  }  \]

Now suppose we have a functor $\boxed{ \boxed{1 | 12} \; G : \calJ \to \leftcat{(l \downarrow {\rightadj R})} }$ (see the center diagram in the large display above).
We form the components of $\boxed{1 | 12} \; G$ by composition, namely
a functor $\rightcat{  \boxed{ \boxed{2} \; {\black G}Q : {\black\calJ} \to \calR }  }$ into $\rightcat\calR$, and
a natural transformation (a cone) $\leftcat{  \boxed{ \boxed{2} \; {\black G}\lambda : l \Rightarrow {\black G}{\rightcat Q}{\rightadj R} : {\black\calJ} \to \calL }  }$ in $\leftcat\calL$.
Suppose now that (the functor $\rightcat{ \boxed{2} \; {\black G}Q : {\black\calJ} \to \calR}$) has
a limiting cone $\rightcat{   \boxed{  \textstyle  \boxed{3 | 21} \; \pi_{\black G Q} : {  \boxed{3|20} \; ({\black G}Q)\lim_\calR  } \Rightarrow {\black G} Q : {\black\calJ} \to \calR   }   }$ in $\rightcat\calR$ (at the upper right of the above large display),
and that (that limiting cone in $\rightcat\calR$) is preserved by $\rightadj R$ (so we are now in the lower right of the above display).
Then there exists a unique (mediating arrow $\leftcat{   \boxed{\textstyle  \boxed{4 | 22} \; {\overline{{\black G}\lambda}} :  l \to \rightadj{ \big(\rightcat{(\black G Q)\lim_\calR}\big) R }  }   }$ in $\leftcat\calL$),  
which is also (a <u>morphism of cones in $\leftcat\calL$</u>)
$\leftcat{    \boxed{  \boxed{4 | 22} \;{\overline{{\black G}\lambda}} : {\black G}\lambda \to {  \rightcat{ \pi_{\black G Q}  }  }{\rightadj R} }    }$ (in the lower right of the display).
But, and here is a crucial but somewhat tricky, perhaps subtle, point, 
(that same data) may.be viewed as (<u><i>a single cone</i> in $(l\downarrow \rightadj R)$</u>)
$\rightadj{  \boxed{\textstyle \boxed{5 | 121} \; \pi_{\black G} : \boxed{5|120} \; \rightcat{\big((\black G Q)\lim_\calR\big)} \leftcat{[\overline{\black G \lambda}]} \Rightarrow \leftcat{ G  :  \calJ \to (l\downarrow \rightadj R) }  }   }$ (shown at the upper left of the above display).
Thus the same arrow $\leftcat{   \boxed{\textstyle  \boxed{4 | 22} \; { \overline{{\black G}\lambda} }  }   }$ plays three different roles:

mediating arrow $\leftcat{   \boxed{\textstyle  \boxed{4 | 22} \; {\overline{{\black G}\lambda}} :  l \to \rightadj{ \big(\rightcat{(\black G Q)\lim_\calR}\big) R }  }   }$ in $\leftcat\calL$

morphism of cones $\leftcat{ \boxed{     \textstyle  \boxed{4 | 22} \; {  \overline{ {\black G}\lambda }  } : \leftcat l [{\black G}\lambda] \to  \Big(  \rightadj{ \big( \rightcat{(\black G Q)\lim_\calR} \big) R }  \Big) [{ \rightcat{ \pi_{\black G Q} } }{\rightadj R} ] }    }$ in $(\Delta \downarrow \ulcorner G\rightcat Q\rightadj R\urcorner)$

a component of the object $ \rightadj{  \boxed{     \textstyle  \boxed{120} \; \rightadj{ \big( \rightcat{(\black G Q)\lim_\calR} \big) }   \leftcat{  \big[ \, \overline{\black G \lambda} \, \big]  }    }     } $  in $\leftcat{  (l \downarrow \rightadj R)  }$

<hr />

Same data but different notation:

\[ \leftcat{ \begin{array} {} && 1 \\ & \llap{!} \nearrow & \red{ \Bigg\downarrow \rlap{ \kern-2.8em \boxed{(G_i[\lambda_i])\lim} } } & \rightcat{ \searrow \rlap{ G_i\lim } }      \\         \calJ & \xrightarrow[\kern3em]{\textstyle {\rightcat G}_i[\lambda_i]} & \boxed{(l \downarrow {\rightadj R})} & \rightcat{ \xrightarrow[\kern3em]{\textstyle Q = r} } & \rightcat\calR \\ && \Bigg\downarrow & \buildrel \textstyle \lambda \over \Longrightarrow & \rightadj{\Bigg\downarrow \rlap R} \\ && 1 & \xrightarrow[\textstyle l]{} & \calL \\ \end{array} } \]

\[ \leftcat{ \boxed{ \begin{array} {cccccc c|cccccc c|cccccc} {} \rlap{ \kern7em (l\downarrow \rightadj R) \kern.5em \rightcat{ \xrightarrow[\kern20em]{\textstyle Q = r} } } &&&&& && {} \rlap{ \kern6em \rightcat\calR \kern.5em \rightadj{ \xrightarrow[\kern27em]{\textstyle R} } } &&&&&&& {} \rlap{ \kern11em \calL }     \\    \hline & \forall \rightcat r[\kappa] & \rightcat{ {} \rlap{ \kern-1em \xrightarrow[\kern12em]{\textstyle \forall \rho_i} } } &&& {\rightcat G}_i[\lambda_i] & \kern1em & \kern1em & \rightcat{\forall r} & \rightcat{ {} \rlap{ \kern-1em \xrightarrow[\kern10em]{\textstyle \forall \rho_i} } } &&& \rightcat{ G_i} & \kern1em & \kern1em &&& {\rightcat r}{\rightadj R} & \rightcat{ {} \rlap{ \kern-1em \xrightarrow [\kern11em] {\textstyle \rho_i \rightadj R } } } &&& \rightcat{G_i} {\rightadj R} & \\ && \rightcat{ \llap{\exists!\rho} \searrow } && \rightcat{ \nearrow \rlap{\pi_i} } & &&& & \rightcat{ \llap{\exists!\rho} \searrow } && \rightcat{ \nearrow \rlap{\pi_i} } &&&&& \llap{\kappa} \nearrow && \llap{\lambda_i} \nearrow && \rightcat{ \nearrow \rlap{\pi_i \rightadj R} } \\ &&& \rightcat{ G_i\lim}[\lambda] && && &&& \rightcat{G_i\lim} &&&&& l & {} \rlap{ \kern-1em \xrightarrow [\textstyle \exists!\lambda] {\kern8em} } &&& \rightcat{G_i\lim}\rightadj R \\ \end{array} } } \] 
We start with a functor ${\rightcat G_i[\leftcat\lambda_i]} : \calJ \to \leftcat{(l\downarrow {\rightadj R})}$, so $\rightcat{ G : \calJ \to \calR}$ is a functor landing in $\rightcat\calR$, while $\{ \leftcat{ \lambda_i : l \rightarrow {\rightcat G_i \rightadj R} } \}_{i\in\calJ}$ is a cone in $\leftcat\calL$.
Suppose $\rightcat G$ has a.limit $\rightcat{\pi_i : G\lim \to G_i}$ in $\rightcat\calR$ which is preserved by $\rightadj R$.
In these circumstances the limit $\rightcat{\pi_i : G\lim \to G_i}$ in $\rightcat\calR$ lifts to a limit in $\leftcat{(l\downarrow \rightadj R)}$.


\[ \leftcat{ \boxed{ \begin{array} {ccccccc c|cccccc c|cccccc} {} \rlap{ \kern8em \calL \kern8em \rightadj{ \xleftarrow[\kern4em]{\textstyle R} } } &&&&&&&&& {} \rlap{ \kern5em \rightcat{ \calR \kern5em \xleftarrow[\kern4em]{\textstyle Q = r} } } &&&&&&& {} \rlap{ \kern4.5em (l\downarrow \rightadj R) } &&&&& test \\ \hline && {\rightcat r}{\rightadj R} & \rightcat{ {} \rlap{ \kern-1em \xrightarrow [\kern11em] {\textstyle \rho_i \rightadj R } } } &&& \rightcat{G_i} {\rightadj R} & \kern1em & \kern1em & \rightcat{\forall r} & \rightcat{ {} \rlap{ \kern-1em \xrightarrow[\kern10em]{\textstyle \forall \rho_i} } } &&& \rightcat{ G_i} & \kern1em & \kern1em & \forall \rightcat r[\mu] & \rightcat{ {} \rlap{ \kern-1em \xrightarrow[\kern12em]{\textstyle \forall \rho_i} } } &&& {\rightcat G}_i[\lambda_i] & test \\ & \llap{\kappa} \nearrow && \llap{\lambda_i} \nearrow && \rightcat{ \nearrow \rlap{\pi_i \rightadj R} } & &&& & \rightcat{ \llap{\exists!\rho} \searrow } && \rightcat{ \nearrow \rlap{\pi_i} } &&& && \rightcat{ \llap{\exists!\rho} \searrow } && \rightcat{ \nearrow \rlap{\pi_i} } && test \\ l & {} \rlap{ \kern-1em \xrightarrow [\textstyle \exists!\lambda] {\kern8em} } &&& \rightcat{G_i\lim}\rightadj R && &&& && \rightcat{G_i\lim} &&& && && \rightcat{ G_i\lim}[\lambda] &&& test \\ \end{array} } } \] 

<hr />
<h3>References</h3>
Kelly 1989 "Elementary observations on 2-categorical limits"
https://doi.org/10.1017%2FS0004972700002781


Below this line is just excess material, basically earlier draft stuff that I am keeping around in case I want to use them again.
<hr />
---------------------

\[ \leftcat{ \boxed{ \begin{array} {cc|ccc|cccc} \calJ \rlap{ \xrightarrow[\kern4.5em \boxed{12} \kern4.5em] {\textstyle \boxed{ \black G = \black G \rightcat Q [\black G \lambda]} }   } & \kern0em & \kern0em & (l\downarrow\calL)  \rlap{  \lower3.2ex{ \kern-2.3em \boxed{10} }  }   \rlap{ \rightcat{ \xrightarrow[ \textstyle \kern3.6em \boxed{11} \; \text{faithful} \kern3.6em ]{\textstyle Q=r} } } & & & & &\calL &   \\      \\      \hline j &&& j\black G = j \big( \black G \rightcat Q [\black G \lambda] \big) = j \black G \rightcat Q [j \black G \lambda] &&&&& j\black G\rightcat Q \\ &&& &&&& \llap{j \black G \lambda} \nearrow & \\ \llap\iota \Bigg\downarrow &&& \llap{\iota \black G = {} } \Bigg\downarrow \rlap{ {} = \iota \black G \rightcat Q } & && l & \iota \black G & \Bigg\downarrow \rlap{\iota \black G \rightcat Q} & \\ &&&& && & \llap{j' \black G \lambda} \searrow & \\ j' &&& j' \black G = j' \big( \black G \rightcat Q [\black G \lambda] \big) = j' \black G \rightcat Q [j' \black G \lambda] &&&&& j' \black G\rightcat Q \\ \end{array} } } \]