# Kerodon

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

Corollary 7.2.1.19. Let $f: X \rightarrow Y$ and $f': X' \rightarrow Y'$ be left cofinal morphisms of simplicial sets. Then the product map $(f \times f'): X \times X' \rightarrow Y \times Y'$ is left cofinal.

Proof. Factoring $f \times f'$ as a composition

$X \times X' \xrightarrow { f \times \operatorname{id}_{X'} } Y \times X' \xrightarrow { \operatorname{id}_{Y} \times f'} Y \times Y',$

the desired result follows by combining Corollary 7.2.1.18 with Proposition 7.2.1.6. $\square$