Kerodon

Proof. The morphism $G$ is right cofinal if and only if, for every left fibration $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$, the projection map $K \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}$ is a weak homotopy equivalence (Corollary 7.2.3.15). By virtue of Variant 8.5.6.10, it suffices to verify this condition in the special case where $\operatorname{\mathcal{E}}= \operatorname{\mathcal{C}}\times _{\operatorname{\mathcal{C}}'} \operatorname{\mathcal{E}}'$ is the pullback of a left fibration $\operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}'$. In this case, the projection map $\operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{E}}'$ is a Morita equivalence (Corollary 8.5.6.15), and therefore a weak homotopy equivalence (Remark 8.5.6.3). It follows that $G$ is right cofinal if and only if, for every left fibration $\operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{C}}'$, the projection map $K \times _{\operatorname{\mathcal{C}}'} \operatorname{\mathcal{E}}' \rightarrow \operatorname{\mathcal{E}}'$ is a weak homotopy equivalence. By virtue of Corollary 7.2.3.15, this is equivalent to the requirement that $F \circ G$ is right cofinal. $\square$