Proposition 7.7.6.7. Let $\lambda $ be an uncountable cardinal, let $\kappa = \mathrm{cf}(\lambda )$ be its cofinality, and let $\operatorname{\mathcal{C}}$ be a $\kappa $-small simplicial set. Suppose we are given a natural transformation $\overline{\gamma }: \overline{\mathscr {F}}' \rightarrow \overline{\mathscr {F}}$ between diagrams $\overline{\mathscr {F}}, \overline{\mathscr {F}}': \operatorname{\mathcal{C}}^{\triangleright } \rightarrow \operatorname{\mathcal{S}}^{< \lambda }$. Assume that $\overline{\mathscr {F}}$ is a colimit diagram and that the natural transformation $\gamma = \overline{\gamma }|_{\operatorname{\mathcal{C}}}$ is cartesian. Then $\overline{\mathscr {F}}'$ is a colimit diagram if and only if the natural transformation $\overline{\gamma }$ is cartesian.
Proof. Write $\overline{\mathscr {F}}$ and $\overline{\mathscr {F}}'$ as the covariant transport representations of left fibrations $\overline{U}: \overline{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{C}}^{\triangleright }$ and $\overline{U}': \overline{\operatorname{\mathcal{E}}}' \rightarrow \operatorname{\mathcal{C}}^{\triangleright }$, respectively. By virtue of Theorem 7.4.2.4, there exists a morphism $\overline{\Gamma } \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleright } }( \overline{\operatorname{\mathcal{E}}}', \overline{\operatorname{\mathcal{E}}} )$ which is compatible with $\overline{\gamma }$, in the sense of Definition 7.4.2.2. Replacing $\overline{U}'$ with an equivalent left fibration if necessary, we may assume that $\overline{\Gamma }$ is an isofibration (Remark 7.7.6.4), and therefore a left fibration (Lemma 7.7.6.3). Set $\operatorname{\mathcal{E}}= \operatorname{\mathcal{C}}\times _{ \operatorname{\mathcal{C}}^{\triangleright } } \overline{\operatorname{\mathcal{E}}}$ and $\operatorname{\mathcal{E}}' = \operatorname{\mathcal{C}}\otimes _{ \operatorname{\mathcal{C}}^{\triangleright } } \overline{\operatorname{\mathcal{E}}}'$, so that $\overline{\Gamma }$ restricts to a left fibration $\Gamma : \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{E}}$. Since $\gamma $ is cartesian, Proposition 7.7.6.5 guarantees that $\Gamma $ is a Kan fibration; moreover, $\overline{\gamma }$ is cartesian if and only if $\overline{\Gamma }$ is also a Kan fibration. Since $\overline{\mathscr {F}}$ is a colimit diagram, Corollary 7.4.3.14 guarantees that the inclusion map $\iota : \operatorname{\mathcal{E}}\hookrightarrow \overline{\operatorname{\mathcal{E}}}$ is a weak homotopy equivalence; moreover, $\overline{\mathscr {F}}'$ is a colimit diagram if and only if the inclusion map $\iota ': \operatorname{\mathcal{E}}' \hookrightarrow \overline{\operatorname{\mathcal{E}}}'$ is a weak homotopy equivalence. We are therefore reduced to showing that $\iota '$ is a weak homotopy equivalence if and only if $\overline{\Gamma }$ is a Kan fibration, which is a restatement of Proposition 7.7.6.2. $\square$