0N85 Lemma 8. For any three objects A,B,Cโ๐A,B,C\in\mathcal{C} and any morphism f:BโBโฒf\colon B\to B^{\prime}, the following cube commutes. AโBโC{\lx@inpgf@ignorespaces ABC}โโAโBโฒโC{\lx@inpgf@ignorespaces AB^{\prime}C}AโCโB{\lx@inpgf@ignorespaces ACB}AโCโBโฒ{\lx@inpgf@ignorespaces ACB^{\prime}}BโCโA{\lx@inpgf@ignorespaces BCA}โBโฒโCโA{\lx@inpgf@ignorespaces B^{\prime}CA}CโBโA{\lx@inpgf@ignorespaces CBA}โCโBโฒโA{\lx@inpgf@ignorespaces CB^{\prime}A}1.{\lx@inpgf@ignorespaces\scriptstyle{1.}}5.{\lx@inpgf@ignorespaces\scriptstyle{5.}}2.{\lx@inpgf@ignorespaces\scriptstyle{2.}}6.{\lx@inpgf@ignorespaces\scriptstyle{6.}}4.{\lx@inpgf@ignorespaces\scriptstyle{4.}}3.{\lx@inpgf@ignorespaces\scriptstyle{3.}} 1.=AโRf,C2.=Rf,CโA3.=RA,RBโฒ,C4.=RA,RB,C5.=RA,Cโf6.=RA,fโC\begin{array}[]{lll}1.\>=\>A\otimes R_{f,C}&2.\>=\>R_{f,C}\otimes A&3.\>=\>R_{A,R_{B^{\prime},C}}\\ 4.\>=\>R_{A,R_{B,C}}&5.\>=\>R_{A,C\otimes f}&6.\>=\>R_{A,f\otimes C}\end{array}
0N86 Proof. This is an special case of the axiom (โโโ)(\bullet\otimes{\Downarrow}) together with (โโโโ)(\bullet\otimes{\to}\to). โ