Corollary 7.2.1.16. Suppose we are given a categorical pushout diagram of simplicial sets
If $f$ is left cofinal, then $f'$ is also left cofinal.
Corollary 7.2.1.16. Suppose we are given a categorical pushout diagram of simplicial sets
If $f$ is left cofinal, then $f'$ is also left cofinal.
Proof. By virtue of Corollary 7.2.1.15, we may assume that $f$ factors as a composition $X \xrightarrow {g} Y \xrightarrow {h} Z$, where $g$ is left anodyne and $h$ is a trivial Kan fibration. Setting $Y' = Y {\coprod }_{X} X'$, we can expand (7.9) to a commutative diagram
Note that the square on the left is a pushout diagram in which the horizontal maps are monomorphisms, and therefore a categorical pushout diagram (Example 4.5.4.12). Applying Proposition 4.5.4.8, we deduce that the square on the right is also a categorical pushout diagram. Since $h$ is a categorical equivalence (Proposition 4.5.3.11), it follows that $h'$ is also a categorical equivalence (Proposition 4.5.4.10). In particular, $h'$ is left cofinal (Corollary 7.2.1.13). The morphism $g'$ is left anodyne (since it is a pushout of $g$), and is therefore also left cofinal (Proposition 7.2.1.3). Applying Proposition 7.2.1.6, we deduce that $f' = h' \circ g'$ is also left cofinal. $\square$