\documentclass{article}

\usepackage[a3paper, margin=1in]{geometry}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{tikz-cd}
\usepackage{mathrsfs}

\DeclareMathOperator{\Sh}{Sh}
\DeclareMathOperator{\Hom}{Hom}
\DeclareMathOperator{\id}{id}


\renewcommand{\qed}{\hfill\blacksquare}

\newtheorem*{lemma}{Lemma}

\tikzset{
  symbol/.style={
    draw=none,
    every to/.append style={
      edge node={node [sloped, allow upside down, auto=false]{$#1$}}}
  }
}

\title{Getting over it with April Grimoire}

\begin{document}

\maketitle

\section{Statement}

Suppose

$$
\begin{tikzcd}
  W \arrow[r, "\beta'"] \arrow[d, "\alpha'"] & X \arrow[d, "\alpha"] \\
  Y \arrow[r, "\beta"] & Z \\
\end{tikzcd}
$$

is a commutative diagram. Given a sheaf $\mathscr{F} \in \Sh(X)$, we can construct the push-pull map $\beta^{-1}\alpha_*\mathscr{F} \to (\alpha')^{-1}\beta'_*\mathscr{F}$ in the following two ways:

(Denote by $\eta_\alpha, \epsilon_{\alpha}$ the unit and counit of the adjoint pair $\alpha^{-1} \dashv \alpha_*$)

\begin{enumerate}
\item
  \begin{tikzcd}
    \Hom(\beta^{-1}\alpha_*\mathscr{F},\alpha'_*(\beta')^{-1}\mathscr{F}) &
    \arrow[l, symbol=\in] \alpha'_*(\beta')^{-1}\epsilon_{\alpha,\mathscr{F}} \circ \eta_{\alpha', \beta^{-1}\alpha_*\mathscr{F}} &
    = & \mathrm{pushpull}_1\\
    \Hom((\alpha')^{-1}\beta^{-1}\alpha_*\mathscr{F},(\beta')^{-1}\mathscr{F}) \arrow[u, "\cong"] & \\
    \Hom((\beta')^{-1}\alpha^{-1}\alpha_*\mathscr{F}, (\beta')^{-1}\mathscr{F}) \arrow[u, "\cong"] & \arrow[l, symbol=\in] (\beta')^{-1}\epsilon_{\alpha,\mathscr{F}} \arrow[uu, mapsto] \\
    \Hom(\alpha^{-1}\alpha_*\mathscr{F}, \mathscr{F}) \arrow[u] & \arrow[l, symbol=\in] \epsilon_{\alpha,\mathscr{F}} \arrow[u, mapsto] \\
    \Hom(\alpha_*\mathscr{F}, \alpha_*\mathscr{F}) \arrow[u, "\cong"] & \arrow[l, symbol=\in] \id_{\alpha_*\mathscr{F}} \arrow[u, mapsto] \\
    \Hom(\mathscr{F},\mathscr{F}) \arrow[u] & \arrow[l, symbol=\in] \id_{\mathscr{F}} \arrow[u, mapsto] \\
  \end{tikzcd}
\item

  \begin{tikzcd}
    \Hom(\beta^{-1}\alpha_*\mathscr{F},\alpha'_*(\beta')^{-1}\mathscr{F}) & \arrow[l, symbol=\in] \epsilon_{\beta,\alpha'_*(\beta')^{-1}\mathscr{F}} \circ \beta^{-1}\alpha_*\eta_{\beta',\mathscr{F}} & = & \mathrm{pushpull}_2\\
    \Hom(\alpha_*\mathscr{F},\beta_*\alpha'_*(\beta')^{-1}\mathscr{F}) \arrow[u, "\cong"] & \\
    \Hom(\alpha_*\mathscr{F},\alpha_*\beta'_*(\beta')^{-1}\mathscr{F}) \arrow[u, "\cong"] & \arrow[l, symbol=\in] \alpha_*\eta_{\beta',\mathscr{F}} \arrow[uu, mapsto] \\
    \Hom(\mathscr{F}, \beta'_*(\beta')^{-1}\mathscr{F}) \arrow[u] & \arrow[l, symbol=\in] \eta_{\beta',\mathscr{F}} \arrow[u, mapsto] \\
    \Hom((\beta')^{-1}\mathscr{F},(\beta')^{-1}\mathscr{F}) \arrow[u, "\cong"] & \arrow[l, symbol=\in] \id_{(\beta')^{-1}\mathscr{F}} \arrow[u, mapsto] \\
    \Hom(\mathscr{F}, \mathscr{F}) \arrow[u] & \arrow[l, symbol=\in] \id_{\mathscr{F}} \arrow[u, mapsto] \\
  \end{tikzcd} 
\end{enumerate}

\section{Solution}

Draw the two push-pull morphisms in the diagram

\begin{tikzcd}[column sep=3cm, row sep=3cm]
  \beta^{-1}\alpha_*\mathscr{F} \arrow[d, "\beta^{-1}\alpha_*\eta_{\beta',\mathscr{F}}"] \arrow[r, "\eta_{\alpha', \beta^{-1}\alpha_*\mathscr{F}}"] &
  \alpha'_*(\alpha')^{-1}\beta^{-1}\alpha_*\mathscr{F} = \alpha'_*(\beta')^{-1}\alpha^{-1}\alpha_*\mathscr{F} \arrow[d, "\alpha'_*(\beta')^{-1}\epsilon_{\alpha,\mathscr{F}}"] \\
  \beta^{-1}\alpha_*\beta'_*(\beta')^{-1}\mathscr{F} = \beta^{-1}\beta_*\alpha'_*(\beta')^{-1}\mathscr{F} \arrow[r, "\epsilon_{\beta,\alpha'_*(\beta')^{-1}\mathscr{F}}"] &
  \alpha'_*(\beta')^{-1}\mathscr{F} \\
\end{tikzcd}

The top and bottom morphisms in the diagram above are morphisms in natural transformations, which encourages us to check the following diagrams, which make use of natuality:

\begin{tikzcd}[column sep=3cm, row sep=3cm]
  \beta^{-1}\alpha_*\mathscr{F} \arrow[d, "\beta^{-1}\alpha_*\eta_{\beta',\mathscr{F}}"] \arrow[r, "\eta_{\alpha', \beta^{-1}\alpha_*\mathscr{F}}"] &
  \alpha'_*(\alpha')^{-1}\beta^{-1}\alpha_*\mathscr{F} \arrow[d, "\alpha'_*(\alpha')^{-1}\beta^{-1}\alpha_*\eta_{\beta',\mathscr{F}}"] \\
  \beta^{-1}\alpha_*\beta'_*(\beta')^{-1}\mathscr{F} \arrow[r, "\eta_{\alpha',\beta^{-1}\alpha_*\beta'_*(\beta')^{-1}}\mathscr{F}"] &
  \alpha'_*(\alpha')^{-1}\beta^{-1}\alpha_*\beta'_*(\beta')^{-1}\mathscr{F} \\
\end{tikzcd}

\begin{tikzcd}[column sep=3cm, row sep=3cm]
  \beta^{-1}\beta_*\alpha'_*(\beta')^{-1}\alpha^{-1}\alpha_*\mathscr{F} \arrow[r, "\epsilon_{\beta,\alpha'_*(\beta')^{-1}\alpha^{-1}\alpha_*\mathscr{F}}"] \arrow[d, "\beta^{-1}\beta_*\alpha'_*(\beta')^{-1}\epsilon_{\alpha,\mathscr{F}}"] &
  \alpha'_*(\beta')^{-1}\alpha^{-1}\alpha_*\mathscr{F} \arrow[d, "\alpha'_*(\beta')^{-1}\epsilon_{\alpha,\mathscr{F}}"] \\ 
  \beta^{-1}\beta_*\alpha'_*(\beta')^{-1}\mathscr{F} \arrow[r, "\epsilon_{\beta,\alpha'_*(\beta')^{-1}\mathscr{F}}"] &
  \alpha'_*(\beta')^{-1}\mathscr{F} \\
\end{tikzcd}

Then there is connecting maps

\begin{tikzcd}
  \beta^{-1}\alpha_*\mathscr{F} \arrow[d, "\beta^{-1}\eta_{\beta,\alpha_*\mathscr{F}}"] \\
  \beta^{-1}\beta_*\beta^{-1}\alpha_*\mathscr{F} \arrow[d, "\beta^{-1}\beta_*\eta_{\alpha', \beta^{-1}\alpha_*\mathscr{F}}"] \\
  \beta^{-1}\beta_*\alpha'_*(\alpha')^{-1}\beta^{-1}\alpha_*\mathscr{F} \arrow[d, equal] \\
  \beta^{-1}\beta_*\alpha'_*(\beta')^{-1}\alpha^{-1}\alpha_*\mathscr{F} \\
\end{tikzcd}

\begin{tikzcd}
  \alpha'_*(\alpha')^{-1}\beta^{-1}\alpha_*\beta'_*(\beta')^{-1}\mathscr{F} \arrow[d, equal] \\
  \alpha'_*(\alpha')^{-1}\beta^{-1}\beta_*\alpha'_*(\beta')^{-1}\mathscr{F} \arrow[d, "\alpha'_*(\alpha')^{-1}\epsilon_{\beta,\alpha'_*(\beta')^{-1}\mathscr{F}}"] \\
  \alpha'_*(\alpha')^{-1}\alpha'_*(\beta')^{-1}\mathscr{F} \arrow[d, "\alpha'_*\epsilon_{\alpha',(\beta')^{-1}\mathscr{F}}"] \\
  \alpha'_*(\beta')^{-1}\mathscr{F}
\end{tikzcd}

\begin{tikzcd}
  \alpha'_*(\alpha')^{-1}\beta^{-1}\alpha_*\beta'_*(\beta')^{-1}\mathscr{F} \arrow[d, equal] \\
  \alpha'_*(\beta')^{-1}\alpha^{-1}\alpha_*\beta'_*(\beta')^{-1}\mathscr{F} \arrow[d, "\alpha'_*(\beta')^{-1}\epsilon_{\alpha,\beta'_*(\beta')^{-1}\mathscr{F}}"] \\
  \alpha'_*(\beta')^{-1}\beta'_*(\beta')^{-1}\mathscr{F} \arrow[d, "\alpha'_*\epsilon_{\beta',(\beta')^{-1}\mathscr{F}}"] \\
  \alpha'_*(\beta')^{-1}\mathscr{F}
\end{tikzcd}

Note that we provided two morphisms $\alpha'_*(\alpha')^{-1}\beta^{-1}\alpha_*\beta'_*(\beta')^{-1}\mathscr{F} \to \alpha'_*(\beta')^{-1}\mathscr{F}$. In fact, these two are identical: they both equal $\alpha'_*\epsilon_{\beta\alpha',(\beta')^{-1}\mathscr{F}}$.
(There is similarly a counterpart for the first connecting map, but I'm too lazy to type it down.) It follows from the following general fact about adjoints:

\begin{lemma}
  For adjoint pairs

  \begin{tikzcd}
    \mathscr{C} \arrow[r, shift left=2px, "F_1"] &
    \mathscr{D} \arrow[l, shift left=2px, "G_1"] \arrow[r, shift left=2px, "F_2"] &
    \mathscr{E} \arrow[l, shift left=2px, "G_2"]
  \end{tikzcd}

  Suppose $F_1\dashv G_1$ with unit and counit $\eta_1, \epsilon_1$,$F_2\dashv G_2$
  with unit and counit $\eta_2, \epsilon_2$.
  Then $F_2F_1\dashv G_1G_2$ with unit and counit

  \begin{tikzcd}
    X \arrow[r, "\eta_{1,X}"] & G_1 F_1 X \arrow[r, "G_1 \eta_{2,F_1 X}"] & G_1 G_2 F_2 F_1 X
  \end{tikzcd}

  \begin{tikzcd}
    F_2 F_1 G_1 G_2 X \arrow[r, "F_2 \epsilon_{1,G_2 X}"] & F_2 G_2 X \arrow[r, "\epsilon_{2, X}"] & X
  \end{tikzcd}
\end{lemma}


With these two maps we can connect the previous two natural transformation diagrams together into a huge diagram:

% https://tikzcd.yichuanshen.de/#N4Igdg9gJgpgziAXAbVABwnAlgFyxMJZABgBpiBdUkANwEMAbAVxiRAB12AjGHOgPWABaAIwBfTozQALOgH0AVJwC2dHNLgBjAE7AAYmJBjS6TLnyEUANnJVajFm0kMZdAOSKAFM9duAlIKiEty8AsLiPrKKKmoaOvqGxqbYeAREAEykAKx29MysiBwhfIERxfJK7FKyHgre5f6lwdVhQZEVMepaugZGJiAYKRZEABzZuQ4FRS219Tx8jeHNLrJN7dHsql3xvUkDZqmWJKRWE-lO5WtVKx0NXpzz7gFLnXE9if2D5mnWJ2eOhXasyBzzalxe11cG0ewIaoLKWzeCT6yW+R0yIhE-ymD1CV0eGxm9zhV0R3WRey+h1GpEx2IuRLquIW8OCZJ2iTsMCgAHN4ERQAAzbQQZRIMggHAQJAiah5AHTG6wmGs17k3rUBh0HgMAAKB2GhQYMEFOBRIGFovF1ClSAALHLJhdHlcWhtQnJgMz3KQ1RzDJrtTA9QafiBjabzZaxYgJbbEJl7OdAeCwQTKh6vZCaqQAATe103Dbs95ifPsTRYbSacsuiGZ72+7O3EsJAPhoMhoZhiNmvbRmU26WILKO5OK3zEmaq1NlN0Zvie71uJutgztrU6-Xdyzhk19-oDxCyyXDgDMY4BYCYDAYga3od3vZA1GkMDoUDYkDArE1WB-bBQBATBcMaUYijGibxheSYKpwMBoNgDAEEu5RNoycyhIsYItIWUKVGuYgbp225omwz79hBSBQcONiwTis7BOmQLEiqVwIUhKFZi0q6xOqREvh2D47mw2hYDy0gHkKVGIDB8YAOyXgxGHLjOHFYMhYCoTxfqloJm7BqR1JGvu4FWogDqnkgo70RcDbNiuBYQvOy6sVhrJsnxHL6SRj6ieJklmTGlnxnR8oFNet73oZfkmZGr7vp+hTfr+4b-lMQEgWBlHmTZClKQySruohGlccupCYSypJeaW5aVtW5YqSS9YlZp2k3E2MJuVVEKEWIAC8LEZq1ZUORVqnVdstWcPVNZDfU07sSNWlZo86FFUyzVBJ5U3ItFXZkYUYkSVJFoyXR+W2Sm6ltatoTrZOm1sb1NVtj5wmHXukZiBQYhAA
\begin{tikzcd}
\beta^{-1}\alpha_*\mathscr{F} \arrow[rrrrrr, "\alpha'_*(\beta')^{-1}\mathscr{F}"] \arrow[dddddd, "{\beta^{-1}\alpha_*\eta_{\beta',\mathscr{F}}}"] \arrow[rrddddd, "{\beta^{-1}\beta_*\eta_{\alpha', \beta^{-1}\alpha_*\mathscr{F}} \circ \beta^{-1}\eta_{\beta,\alpha_*\mathscr{F}}}"] &  &                                                                                                                                                                                                                                                           &  &  &  & \alpha'_*(\alpha')^{-1}\beta^{-1}\alpha_*\mathscr{F} \arrow[dddddd, "{\alpha'_*(\alpha')^{-1}\beta^{-1}\alpha_*\eta_{\beta',\mathscr{F}}}"] \arrow[rrddddd, no head, Rightarrow]                                                                                                                                                                                        &  &                                                                                                                              \\
                                                                                                                                                                                                                                                                                       &  &                                                                                                                                                                                                                                                           &  &  &  &                                                                                                                                                                                                                                                                                                                                                                         &  &                                                                                                                              \\
                                                                                                                                                                                                                                                                                       &  &                                                                                                                                                                                                                                                           &  &  &  &                                                                                                                                                                                                                                                                                                                                                                         &  &                                                                                                                              \\
                                                                                                                                                                                                                                                                                       &  &                                                                                                                                                                                                                                                           &  &  &  &                                                                                                                                                                                                                                                                                                                                                                         &  &                                                                                                                              \\
                                                                                                                                                                                                                                                                                       &  &                                                                                                                                                                                                                                                           &  &  &  &                                                                                                                                                                                                                                                                                                                                                                         &  &                                                                                                                              \\
                                                                                                                                                                                                                                                                                       &  & \beta^{-1}\beta_*\alpha'_*(\beta')^{-1}\alpha^{-1}\alpha_*\mathscr{F} \arrow[rrrrrr, "{\epsilon_{\beta,\alpha'_*(\beta')^{-1}\alpha^{-1}\alpha_*\mathscr{F}}}"] \arrow[dddddd, "{\beta^{-1}\beta_*\alpha'_*(\beta')^{-1}\epsilon_{\alpha,\mathscr{F}}}"'] &  &  &  &                                                                                                                                                                                                                                                                                                                                                                         &  & \alpha'_*(\beta')^{-1}\alpha^{-1}\alpha_*\mathscr{F} \arrow[dddddd, "{\alpha'_*(\beta')^{-1}\epsilon_{\alpha,\mathscr{F}}}"] \\
\beta^{-1}\alpha_*\beta'_*(\beta')^{-1}\mathscr{F} \arrow[rrrrrr, "{\eta_{\alpha',\beta^{-1}\alpha_*\beta'_*(\beta')^{-1}}\mathscr{F}}"'] \arrow[rrddddd, no head, Rightarrow]                                                                                                         &  &                                                                                                                                                                                                                                                           &  &  &  & \alpha'_*(\alpha')^{-1}\beta^{-1}\alpha_*\beta'_*(\beta')^{-1}\mathscr{F} \arrow[rrddddd, "{\alpha'_*\epsilon_{\beta',(\beta')^{-1}\mathscr{F}} \circ \alpha'_*(\beta')^{-1}\epsilon_{\alpha,\beta'_*(\beta')^{-1}\mathscr{F}}=\alpha'_*\epsilon_{\alpha',(\beta')^{-1}\mathscr{F}} \circ \alpha'_*(\alpha')^{-1}\epsilon_{\beta,\alpha'_*(\beta')^{-1}}\mathscr{F}}"'] &  &                                                                                                                              \\
                                                                                                                                                                                                                                                                                       &  &                                                                                                                                                                                                                                                           &  &  &  &                                                                                                                                                                                                                                                                                                                                                                         &  &                                                                                                                              \\
                                                                                                                                                                                                                                                                                       &  &                                                                                                                                                                                                                                                           &  &  &  &                                                                                                                                                                                                                                                                                                                                                                         &  &                                                                                                                              \\
                                                                                                                                                                                                                                                                                       &  &                                                                                                                                                                                                                                                           &  &  &  &                                                                                                                                                                                                                                                                                                                                                                         &  &                                                                                                                              \\
                                                                                                                                                                                                                                                                                       &  &                                                                                                                                                                                                                                                           &  &  &  &                                                                                                                                                                                                                                                                                                                                                                         &  &                                                                                                                              \\
                                                                                                                                                                                                                                                                                       &  & \beta^{-1}\beta_*\alpha'_*(\beta')^{-1}\mathscr{F} \arrow[rrrrrr, "{\epsilon_{\beta,\alpha'_*(\beta')^{-1}\mathscr{F}}}"]                                                                                                                                 &  &  &  &                                                                                                                                                                                                                                                                                                                                                                         &  & \alpha'_*(\beta')^{-1}\mathscr{F}                                                                                           
\end{tikzcd}

Viewing the diagram as a cube, the front and back faces are already proven to commute. If we can verify commutativity of the two more parrallelograms around $\alpha'_*(\beta')^{-1}\mathscr{F}$, the main result follows directly.

First we inspect the bottom parrallelogram:

% https://tikzcd.yichuanshen.de/#N4Igdg9gJgpgziAXAbVABwnAlgFyxMJZABgBpiBdUkANwEMAbAVxiRAB12AjGHOgPWABaAIwBfTozQALOgH0AVJx58A5IoAUy3nVUBKQaInsAtnRzS4AYwBOwAGJiQY0uky58hFADZyVWowsbJIMMrqaIWH6huLafDHGUrKKceEKWtw60cKxpuaWtg5OLm7YeAREZN7+9MysiByZ8TnGKvJK7ElpGW3ZRpxmFtZ2js6uIBhlnkS+1dS1QQ2RsurpqX25gwUjxeOTHhUoIqQATDWB9SAABMvdtxutOgmpKZ2hKxFNugYtA-nDRTGpQOXmQAFZTuc6sE3lFPl0HvdPr0fv08kNCqMShN3OVQQBmUgAFihi0aCORWVRm3+mOK-hgUAA5vAiKAAGY2CAmJBkEA4CBIY4BaFLdg6OTAe6kVLPWHJDq9SlqaliYxbAGjagMOg8BgABVx0waNiwTOkOCBIE53N51AFSBO8wuSDATAYDG1upgBqNhxADBg7Mt1GkMDoUDYkDArG1WBjbCgECYXEDVptPMQwodiEJIrJSI6MDQ2AYBEl0p6VLlGrpYhu7CsWBsVgbFLW8u+cuLpfLUq+Ms7qyrKoS6tpOxAXr1hqm-sDwfTXMzTv5gtzztFjR7WDLYArA8LI67v3R2yKTmnPtnILYC8t2IzQvt66JcYTDSTKbTofDkcQboevadC7lGBCsI+y5IG+a5IBC+aXEe9yqpwO57gebSDu2x4POOGKTpBtqIPBOa+AhMLtqhJa7n2lbrChZ6amqS5EauOYwQsiHinwB4IoObRym0rzYfRNYTheU4Bt6vpzl4ICmuaD7jE+G6wcRm4Ftx8j9nxSFfIijF1pJDDxpcX6prGIBhhGrrup6-IgQwYEJoRmZ5qR75mcmFmSdZ-7gOBkl8KBDTRhBylQYgMEeQGpmJhAOA4IyzgUGIQA
\begin{tikzcd}
\beta^{-1}\alpha_*\beta'_*(\beta')^{-1}\mathscr{F} \arrow[rrrrrr, "{\eta_{\alpha',\beta^{-1}\alpha_*\beta'_*(\beta')^{-1}}\mathscr{F}}"'] \arrow[dddddd, no head, Rightarrow]                                   &                                                                                                                                                                                             &  &                                   &  &                                                                                                                                 & \alpha'_*(\alpha')^{-1}\beta^{-1}\alpha_*\beta'_*(\beta')^{-1}\mathscr{F} \arrow[dddddd, "{\alpha'_*\epsilon_{\alpha',(\beta')^{-1}\mathscr{F}} \circ \alpha'_*(\alpha')^{-1}\epsilon_{\beta,\alpha'_*(\beta')^{-1}}\mathscr{F}}"] \arrow[llllldd, Rightarrow] \\
                                                                                                                                                                                                                &                                                                                                                                                                                             &  &                                   &  &                                                                                                                                 &                                                                                                                                                                                                                                                                \\
                                                                                                                                                                                                                &  \alpha'_*(\alpha')^{-1}\beta^{-1}\beta_*\alpha'_*(\beta')^{-1}\mathscr{F} \arrow[rrrr, "{\alpha'_*(\alpha')^{-1}\epsilon_{\beta,\alpha'_*(\beta')^{-1}}\mathscr{F}}"] \arrow[rrdd, dotted] &  &                                   &  & \alpha'_*(\alpha')^{-1}\alpha'_*(\beta')^{-1}\mathscr{F} \arrow[lldd, "{\alpha'_*\epsilon_{\alpha',(\beta')^{-1}\mathscr{F}}}"] &                                                                                                                                                                                                                                                                \\
                                                                                                                                                                                                                &                                                                                                                                                                                             &  &                                   &  &                                                                                                                                 &                                                                                                                                                                                                                                                                \\
                                                                                                                                                                                                                &                                                                                                                                                                                             &  & \alpha'_*(\beta')^{-1}\mathscr{F} &  &                                                                                                                                 &                                                                                                                                                                                                                                                                \\
                                                                                                                                                                                                                &                                                                                                                                                                                             &  &                                   &  &                                                                                                                                 &                                                                                                                                                                                                                                                                \\
\beta^{-1}\beta_*\alpha'_*(\beta')^{-1}\mathscr{F} \arrow[rrrrrr, "{\epsilon_{\beta,\alpha'_*(\beta')^{-1}\mathscr{F}}}"] \arrow[ruuuu, "{\eta_{\alpha',\beta^{-1}\beta_*\alpha'_*(\beta')^{-1}\mathscr{F}}}"'] &                                                                                                                                                                                             &  &                                   &  &                                                                                                                                 & \alpha'_*(\beta')^{-1}\mathscr{F} \arrow[luuuu, "{\eta_{\alpha',\alpha'_*(\beta')^{-1}\mathscr{F}}}", Rightarrow] \arrow[llluu, no head, Rightarrow]                                                                                                          
\end{tikzcd}

Where the dotted arrow is just the composition to make the middle triangle commute. Hopefully the reader is able to make sense of why each cell commutes, somewhere using the equational property of unit and counit. I hope to make this clearer, however I am not good at typesetting commutative diagrams.

Likewise, we can verify the parallelogram in the right of the "cube" commutes:

% https://tikzcd.yichuanshen.de/#N4Igdg9gJgpgziAXAbVABwnAlgFyxMJZABgBpiBdUkANwEMAbAVxiRAB13G0ALOgcgD6AKgAUnbn34BKAHrAAtAEYAvpwBGMHHXnK1XBrzojOAWzo4ecAMYAnYADEVIFaXSZc+QigBs5KrSMLGwShlIi4uya2jK6qqFGcfqSxsJmFlZ2js6u7th4BERkPgH0zKyIHAZGQmIJUnKK8VFaOk3JYakarbWR0QKNeumWNvZOLm4gGPleRH4l1GXBlfUCEd0xg83mI1njuVMeBd7IAEykp6VBFVUpvRsDSatP1XwmLTHrH4-tw5ljOUm008hRQAGZSABWK7lEKvNZ1b6xX5Ir79ZFDdg7f7ZCZ5EEnc4AFhhy1unXuSK2+nRaJ61L+o1xB2BxyIkNIYNJN1WlPRDNRiP5L2xTP2ARgUAA5vAiKAAGa2CCmJBkEA4CBIc6BWEreGUu4C-ovFLvVqCYAPfikRl7FTOagMOiaBgABSOs0qDBg8pweJAiuVquoGqQSkW1yQYCYDAYjudMDdHtBIG9vpA1B4MDoUDYkDArEdWALbCgECY6m9-sDKsQ4fVmsQEJ1ZN5dM2LxgaGwDAIFtWNqxGTF9ozqYTSZmKbTfoONa1IcbzaWPP1Zu7WF7YH7SNIfXpIuHdpUAAJONYsLZrGe10KDyiuz2+5b4YPaXeOyjRcex06Xe6p28EBbCwKUeFnSZ50QbVQ0QIkixLSoywrKtM2zXNEGjWMQzoTc8wIVg5yVWt4IbJBISIoNEA5MimwjXVyRqdcn23F90T3K0BW-AFAQVYiw0XJBSJXOE7nbH5MRSE1OjNbQd3Y20eOrfi6NogB2ejW1vfdP0xc02J6QduOyXiAxU0jYLUyjaw02iaIYYsbmQytCxALMc3wkscLwyp80IigVCAA
\begin{tikzcd}
\alpha'_*(\alpha')^{-1}\beta^{-1}\alpha_*\mathscr{F} \arrow[dddddd, "{\alpha'_*(\alpha')^{-1}\beta^{-1}\alpha_*\eta_{\beta',\mathscr{F}}}"] \arrow[rrrrrr, no head, Rightarrow]                                                                              &  &                                                                                                     &                                                                                                                              &  &                                                                                          & \alpha'_*(\beta')^{-1}\alpha^{-1}\alpha_*\mathscr{F} \arrow[dddddd, "{\alpha'_*(\beta')^{-1}\epsilon_{\alpha,\mathscr{F}}}"] \arrow[lllldd, "{\alpha'_*(\beta')^{-1}\alpha^{-1}\alpha_*\eta_{\beta',\mathscr{F}}}"] \\
                                                                                                                                                                                                                                                             &  &                                                                                                     &                                                                                                                              &  &                                                                                          &                                                                                                                                                                                                                     \\
                                                                                                                                                                                                                                                             &  & \alpha'_*(\beta')^{-1}\alpha^{-1}\alpha_*\beta'_*(\beta')^{-1}\mathscr{F} \arrow[rddd] \arrow[rrrd] &                                                                                                                              &  &                                                                                          &                                                                                                                                                                                                                     \\
                                                                                                                                                                                                                                                             &  &                                                                                                     &                                                                                                                              &  & \alpha'_*(\beta')^{-1}\beta'_*(\beta')^{-1}\mathscr{F} \arrow[lldd, no head, Rightarrow] &                                                                                                                                                                                                                     \\
                                                                                                                                                                                                                                                             &  & \alpha'_*(\beta')^{-1}\beta'_*(\beta')^{-1}\mathscr{F}                                              &                                                                                                                              &  &                                                                                          &                                                                                                                                                                                                                     \\
                                                                                                                                                                                                                                                             &  &                                                                                                     & \alpha'_*(\beta')^{-1}\beta'_*(\beta')^{-1}\mathscr{F} \arrow[rrrd, "{\alpha'_*\epsilon_{\beta',(\beta')^{-1}\mathscr{F}}}"] &  &                                                                                          &                                                                                                                                                                                                                     \\
\alpha'_*(\alpha')^{-1}\beta^{-1}\alpha_*\beta'_*(\beta')^{-1}\mathscr{F} \arrow[rrrrrr, "{\alpha'_*\epsilon_{\beta',(\beta')^{-1}\mathscr{F}} \circ \alpha'_*(\beta')^{-1}\epsilon_{\alpha,\beta'_*(\beta')^{-1}\mathscr{F}}}"'] \arrow[rruuuu, Rightarrow] &  &                                                                                                     &                                                                                                                              &  &                                                                                          & \alpha'_*(\beta')^{-1}\mathscr{F} \arrow[luuu, "{\alpha'_*(\beta')^{-1}\eta_{\beta',\mathscr{F}}}"]                                                                                                                
\end{tikzcd}

\qed

\end{document}