Proposition 11.10.2.3. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a locally cartesian fibration of categories which is equipped with a cleavage $(f,Y) \mapsto \widetilde{f}_{Y}$. Suppose we are given a pair of morphisms $f: B \rightarrow C$ and $g: C \rightarrow D$ in the category $\operatorname{\mathcal{C}}$. Then there is a unique natural transformation $\mu _{f,g}: f^{\ast } \circ g^{\ast } \rightarrow (g \circ f)^{\ast }$ of functors from $\operatorname{\mathcal{E}}_{D}$ to $\operatorname{\mathcal{E}}_{B}$ with the following property:
For every object $Y \in \operatorname{\mathcal{E}}_{D}$, the diagram
11.16
\begin{equation} \begin{gathered}\label{equation:characterize-composition-constraint} \xymatrix@R =50pt@C=50pt{ f^{\ast }( g^{\ast }(Y) ) \ar [r]^-{ \widetilde{f}_{ g^{\ast }(Y) } } \ar [d]^-{ \mu _{f,g}(Y) } & g^{\ast }(Y) \ar [d]^-{ \widetilde{g}_ Y} \\ (g \circ f)^{\ast }(Y) \ar [r]^-{ \widetilde{g \circ f}_{Y} } & Y } \end{gathered} \end{equation}
commutes in the category $\operatorname{\mathcal{E}}$.
Proof.
For each object $Y \in \operatorname{\mathcal{E}}_{D}$, our assumption that $\widetilde{ g \circ f}_{Y}$ is locally $U$-cartesian guarantees that there exists a unique morphism $\mu _{f,g}(Y): f^{\ast }( g^{\ast }(Y) ) \rightarrow (g \circ f)^{\ast }(Y)$ in the category $\operatorname{\mathcal{E}}_{B}$ for which the diagram (11.16) is commutative. We will complete the proof by showing that the construction $Y \mapsto \mu _{f,g}(Y)$ is a natural transformation. Let $u: X \rightarrow Y$ be a morphism in the category $\operatorname{\mathcal{E}}_{D}$. We wish to show that the left square in the diagram
\[ \xymatrix@R =50pt@C=50pt{ f^{\ast }( g^{\ast }(X) ) \ar [r]^-{ f^{\ast }(g^{\ast }(u) ) } \ar [d]^-{ \mu _{f,g}(X)} & f^{\ast }(g^{\ast }(Y) ) \ar [d]^-{ \mu _{f,g}(Y) } \ar [r]^-{ \widetilde{f}_{ g^{\ast } Y} } & g^{\ast }(Y) \ar [d]^-{ \widetilde{g}_{Y} } \\ (g \circ f)^{\ast }(X) \ar [r]^-{ (g \circ f)^{\ast }(u) } & (g \circ f)^{\ast }(Y) \ar [r]^-{ \widetilde{g \circ f}_{Y} } & Y } \]
is commutative. Since the square on the right commutes (by the definition of $\mu _{f,g}(Y)$) and the morphism $\widetilde{g \circ f}_{Y}$ is locally $U$-cocartesian, it will suffice to verify the commutativity of the outer rectangle. This fits into another diagram
\[ \xymatrix@R =50pt@C=50pt{ f^{\ast }( g^{\ast }(X) ) \ar [r]^-{ \widetilde{f}_{ g^{\ast }(X)} } \ar [d]^-{ \mu _{f,g}(X)} & g^{\ast }(X) \ar [r]^-{ g^{\ast }(u) } \ar [d]^-{ \widetilde{g}_{X} } & g^{\ast }(Y) \ar [d]^-{ \widetilde{g}_{Y} } \\ (g \circ f)^{\ast }(X) \ar [r]^-{ \widetilde{g \circ f}_{X} } & X \ar [r]^-{ u } & Y, } \]
where the square on the left commutes (by the definition of $\mu _{f,g}(X)$) and the square on the right commutes (by the definition of $g^{\ast }(u)$).
$\square$