Kerodon

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.6.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.13). $\square$