Spahn mates

$$K(a,b')(\diamond_l x,y \Box_l) \cong K(b,a')(x \Box_r,\diamond_r y)$$

$$\array{ a & \overset{x}{\to} & a' \\ \mathllap{\Box_l} \downarrow & \mathllap{\lambda} \Downarrow & \downarrow \mathrlap{\diamond_l} \\ b & \underset{y}{\to} & b' } \;\;\;\;\; \mapsto \;\;\;\;\; \array{ b & \overset{\Box_r}{\to} & a & \overset{x}{\to} & a' & \overset{1}{\to} & a' \\ \mathllap{1} \downarrow & \mathllap{\epsilon} \Downarrow & \mathllap{\Box_l} \downarrow & \mathllap{\lambda} \Downarrow & \downarrow \mathrlap{\diamond_l} & \Downarrow \mathrlap{\eta'} & \downarrow \mathrlap{1} \\ b & \underset{1}{\to} & b & \underset{y}{\to} & b' & \underset{\diamond_r}{\to} & a' }$$

and

$$\array{ b & \overset{y}{\to} & b' \\ \mathllap{\Box_r} \downarrow & \Uparrow & \downarrow \mathrlap{\diamond_r} \\ a & \underset{x}{\to} & a' } \;\;\;\;\; \mapsto \;\;\;\;\; \array{ a & \overset{\Box_l}{\to} & b & \overset{y}{\to} & b' & \overset{1}{\to} & b' \\ \mathllap{1} \downarrow & \mathllap{\eta} \Uparrow &\downarrow & \mathllap{\Box_r} \Uparrow & \downarrow \mathrlap{\diamond_r} & \Uparrow \mathrlap{\epsilon'} & \downarrow \mathrlap{1} \\ a & \underset{1}{\to} & a & \underset{x}{\to} & a' & \underset{\diamond_l}{\to} & b' }$$

That this is a bijection follows from the triangle identities?. The 2-cells $\lambda$ and $\Box_r$ are called mates (or sometimes conjugates) with respect to the adjunctions $\Box_l \dashv \Box_r$ and $\diamond_l \dashv \diamond_r$ (and to the 1-cells $x$ and $y$).

Properties

Strict 2-functors preserve adjurnctions and pasting diagrams, so that i\Box_l $F \colon K \to J$ is a 2-\Box_l\Box_rnctor and i\Box_l $\lambda$ and $\Box_r$ are mates wrt $\Box_l \dashv \Box_r$ and $\diamond_l \dashv \diamond_r$ in $K$, then $F \lambda$ and $F \Box_r$ are mates wrt $F \Box_l \dashv F \Box_r$ and $F \diamond_l \dashv F \diamond_r$ in $J$.

I\Box_l $\alpha \colon F \Rightarrow G$ is a 2-nat\Box_rral trans\Box_lormation?, then the nat\Box_rrality identities $\alpha_b \circ F \Box_l = G \Box_l \circ \alpha_a$ and $\alpha_a \circ F \Box_r = G \Box_r \circ \alpha_b$ are mates wrt $F \Box_l \dashv F \Box_r$ and $G \Box_l \dashv G \Box_r$.