# Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$

Corollary 7.2.1.18. Let $f: X \rightarrow Z$ be a left cofinal morphism of simplicial sets. Then, for every simplicial set $K$, the product map $(f \times \operatorname{id}_ K): X \times K \rightarrow Z \times K$ is left cofinal.

Proof. By virtue of Corollary 7.2.1.14, the morphism $f$ factors as a composition $X \xrightarrow {f'} Y \xrightarrow {f''} Z$, where $f'$ is left anodyne and $f''$ is a trivial Kan fibration. It follows that $f \times \operatorname{id}_{K}$ factors as a composition

$X \times K \xrightarrow {f' \times \operatorname{id}_ K} Y \times K \xrightarrow {f'' \times \operatorname{id}_ K } Z \times K.$

We now note that $f' \times \operatorname{id}_{K}$ is left anodyne (Proposition 4.2.5.3) and $f'' \times \operatorname{id}_{K}$ is a trivial Kan fibration (Remark 1.4.5.2). Applying Corollary 7.2.1.14, we deduce that $f \times \operatorname{id}_{K}$ is left cofinal. $\square$