# Kerodon

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

Proposition 7.2.1.20. Let $f: A \rightarrow B$ and $g: B \rightarrow C$ be morphisms of simplicial sets, and suppose that $g$ is a categorical equivalence. Then $f$ is left cofinal if and only if $g \circ f$ is left cofinal.

Proof. Since $g$ is a categorical equivalence, the construction $\widetilde{C} \mapsto B \times _{C} \widetilde{C}$ induces a bijection from equivalence classes of left fibrations over $C$ to equivalence classes of left fibrations over $B$ (Corollary 5.7.0.6). It follows that $f$ is left cofinal if and only if it satisfies the following condition:

$(\ast )$

For every left fibration $q: \widetilde{C} \rightarrow C$, the restriction map $f^{\ast }: \operatorname{Fun}_{/C}(B, \widetilde{C} ) \rightarrow \operatorname{Fun}_{/C}( A, \widetilde{C} )$ is a homotopy equivalence of Kan complexes.

It will therefore suffice to show that, for every left fibration $q: \widetilde{C} \rightarrow C$, the restriction map $f^{\ast }: \operatorname{Fun}_{/C}(B, \widetilde{C} ) \rightarrow \operatorname{Fun}_{/C}( A, \widetilde{C} )$ is a homotopy equivalence if and only if the restriction map $(g \circ f)^{\ast }: \operatorname{Fun}_{/C}( C, \widetilde{C})\rightarrow \operatorname{Fun}_{/C}( A, \widetilde{C})$ is a homotopy equivalence. This is clear, since our assumption that $g$ is a categorical equivalence guarantees that the restriction map $g^{\ast }: \operatorname{Fun}_{/C}(C, \widetilde{C}) \rightarrow \operatorname{Fun}_{/C}(B, \widetilde{C} )$ is a homotopy equivalence (Corollary 7.2.1.12). $\square$