ScalingStacks

Proof. The 1-equivalences $R_{A,B}$ and 2-isomorphisms $R_{f,B}$ and $R_{A,g}$ comprise the pseudonatural equivalence $R\colon\otimes\to\otimes^{\rm op}$, and conditions $({\to}\otimes{\to})$, $({\bullet}\otimes{\Downarrow})$, $({\Downarrow}\otimes{\bullet})$, $(\to{\to}\otimes{\bullet})$ and $({\bullet}\otimes{\to}\to)$ state that it is indeed a pseudonatural transformation. The 2-morphisms $\tilde{R}_{(A|B,C)}$ and $\tilde{R}_{(A,B|C)}$ comprise the invertible modifications $\tilde{R}_{(-|-,-)}$ and $\tilde{R}_{(-,-|-)}$, and the commuting triangular prisms state that these are indeed modifications, expressing naturality in each argument. The remaining 4 conditions come from Definition 6. ∎