What is the proof of the compatibility of a braiding with the unitors? I am specifically referencing the property that, given a braided monoidal category with a braiding $c$ and left and right unitors $\lambda, \rho$,
$$
\lambda_A \circ c_{A,I}=\rho_{A},
$$
for any object $A$. This equation is stated in almost every reference (first done so by Joyal and Street) defining a braided category, yet an explicit or reproducible proof is, to my knowledge, not given anywhere. The closest thing to a proof I can find is a series of hints on Mathematics SE asked in 2014, however this answer (by Turion) has several inconsistencies/typos, making it hard to understand. Is there some reference where this proof is actually 'spelled out'? How can one prove this relation given the braided monoidal category axioms?
 A: Using the notation of Joyal and Street §2, here’s a proof of $\newcommand{\r}{\rho}\newcommand{\l}{\lambda}\newcommand{\x}{\otimes}\newcommand{\comp}{\!\!\cdot\!}\r_A = \l_A \comp c_{A,I}$.  Since $\l$ and $c$ are invertible, it suffices to prove $\r_A \comp (\l_A \comp c_{A,I} \x I) = \l_A \comp c_{A,I} \comp(\l_A \comp c_{A,I} \x I)$.  Notation: I will write composition as $\comp$, and it binds tighter than $\x$; and will write all associators just as $\alpha$, to reduce clutter.  I’ll black-box details of steps that are purely about symm. mon. cats., not involving the braiding — these are most easily seen using coherence for SMC’s.
$$\begin{align}
 \r_A \comp (\l_A \comp c_{A,I} \x I)
  &= (\l_A \comp c_{A,I}) \comp \r_{A \x I} & \text{naturality of $\r$} \\
  &= \l_A \comp c_{A,I} \comp (A \x \r_I) \comp \alpha & \text{SMC facts}\\
  &= \l_A \comp (\r_I \x A) \comp c_{A,I \x I} \comp \alpha & \text{naturality of $c$}\\
  &= \l_A \comp (\r_I \x A) \comp \alpha \comp (I \x c_{A,I}) \comp \alpha \comp (c_{A,I} \x I) & \text{axiom (B1)} \\
  &= \l_A \comp (I \x \l_A) \comp (I \x c_{A,I}) \comp \alpha \comp (c_{A,I} \x I) & \text{SMC facts}\\
  &= \l_A \comp (I \x \l_A \comp c_{A,I}) \comp \alpha \comp (c_{A,I} \x I)  & \text{functoriality of $\x$}\\
  &= (\l_A \comp c_{A,I}) \comp \l_{A \x I} \comp \alpha \comp (c_{A,I} \x I) & \text{naturality of $\l$}\\
  &= (\lambda_A \comp c_{A,I}) \comp (\lambda_A \x I) \comp (c_{A,I} \x I) & \text{SMC facts}\\
  &= (\lambda_A \comp c_{A,I}) \comp (\lambda_A \comp c_{A,I} \x I) & \text{functoriality of $\x$}
\end{align}
$$
I found this proof using string diagrams, writing down (B1) for $A,I,I$ (as Joyal and Street suggest), and then contemplating how to connect that to the desired equation.
A: A completely spelled out diagrammatic proof is given in Proposition 1.3.21 of Volume II of Bimonoidal Categories, $E_n$-Monoidal Categories, and Algebraic K-Theory by Niles Johnson and Donald Yau.
