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}  }  \]