Kerodon

Proof. We wish to show that the composition map $\operatorname{Hom}_{\operatorname{\mathcal{C}}}(Y, C) \xrightarrow { \circ [q] } \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,C)$ is a homotopy equivalence of Kan complexes. Since $C$ is subterminal, both mapping spaces are either empty or contractible. It will therefore suffice to show that if $\operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,C)$ is nonempty, then $\operatorname{Hom}_{\operatorname{\mathcal{C}}}(Y,C)$ is also nonempty.

Let $\operatorname{\mathcal{C}}^{0}_{/Y}$ be the sieve generated by $q$. Since $q$ is a quotient morphism, $Y$ is a colimit of the diagram

that is, it can be lifted to an initial object $\widetilde{Y}$ of the coslice $\infty $-category $\operatorname{\mathcal{C}}_{F/}$. Since $C \in \operatorname{\mathcal{C}}$ is subterminal, the projection map $U: \operatorname{\mathcal{C}}_{/C} \rightarrow \operatorname{\mathcal{C}}$ restricts to a trivial Kan fibration from $\operatorname{\mathcal{C}}_{/C}$ to a sieve $\operatorname{\mathcal{C}}^{1} \subseteq \operatorname{\mathcal{C}}$. The assumption that $\operatorname{Hom}_{\operatorname{\mathcal{C}}}(X, C)$ is nonempty guarantees that $F$ takes values in $\operatorname{\mathcal{C}}^{1}$ and therefore factors through $\operatorname{\mathcal{C}}_{/C}$. A choice of factorization determines a lift of $C$ to an object $\widetilde{C} \in \operatorname{\mathcal{C}}_{F/}$. Since $\widetilde{Y}$ is an initial object of $\operatorname{\mathcal{C}}_{F/}$, we can choose a morphism $\widetilde{u}: \widetilde{Y} \rightarrow \widetilde{C}$ in the $\infty $-category $\operatorname{\mathcal{C}}_{F/}$. Applying the forgetful functor $\operatorname{\mathcal{C}}_{F/} \rightarrow \operatorname{\mathcal{C}}$, we obtain a morphism $u: Y \rightarrow C$ in $\operatorname{\mathcal{C}}$. $\square$