Kerodon

Definition 7.2.1.1 (Joyal). Let $f: A \rightarrow B$ be a morphism of simplicial sets. We say that $f$ is left cofinal if, for every left fibration $q: \widetilde{B} \rightarrow B$, precomposition with $f$ induces a homotopy equivalence of Kan complexes $\operatorname{Fun}_{/B}( B, \widetilde{B} ) \rightarrow \operatorname{Fun}_{/B}(A, \widetilde{B} )$ (see Corollary 4.4.2.5). We say that $f$ is right cofinal if, for every right fibration $q: \widetilde{B} \rightarrow B$, precomposition with $f$ induces a homotopy equivalence of Kan complexes $\operatorname{Fun}_{/B}( B, \widetilde{B} ) \rightarrow \operatorname{Fun}_{/B}(A, \widetilde{B} )$.