Strongly final vertex $Y$ in a simplicial set gives a retraction of $\mathcal{C}^{ \triangleright }$ onto $\mathcal{C}$

Question

I have a question about a proof from Jacob Lurie's Higher Topos Theory (p 45):

Proposition 1.2.12.5. Let $\mathcal{C}$ be a simplicial set. Every strongly final object (see below what means) of $\mathcal{C}$ is a final object of $\mathcal{C}$. The converse holds if $\mathcal{C}$ is an $\infty$-category.

Proof: Let $[0]$ denote the category with a single object and a single morphism. Suppose that $Y$ is a strongly final vertex of $\mathcal{C}$. Then there exists a retraction of $\mathcal{C}^{ \triangleright }$ onto $\mathcal{C}$ carrying the cone point to $Y$ . Consequently, we obtain a retraction of (H-enriched) homotopy categories from $h\mathcal{C} * [0]$ to $h\mathcal{C}$ carrying the unique object of $[0]$ to $Y$ . This implies that $Y$ is final in $h\mathcal{C}$, so that $Y$ is a final object of $\mathcal{C}$.

(The converse part in the proof I understand)

On used notations:
-$\mathcal{C}^{ \triangleright }$ is the right cone defined to be the join $\mathcal{C} * \Delta^0$.
-Definition 1.2.12.3.: A vertex $X$ of simplicial set $\mathcal{C}$ is called strongly final if the projection $ \mathcal{C}_{/ X} \to \mathcal{C}$ is a trivial fibration of simplicial sets. In other words if any map $f_0 : \partial \Delta^n \to \mathcal{C}$ such that $f_0(n) = X$ can be extended to a map $f : \Delta^n \to \mathcal{C}$.

Question: Why does the assumption that $Y$ is a strongly final vertex of $\mathcal{C}$ imply that there exists a retraction of $\mathcal{C}^{ \triangleright }$ onto $\mathcal{C}$ carrying the cone point to $Y$? Can its construction be given explicitly or (if not) which abstract result is involved to deduce the existence of this retraction?

Answer 1

I think this can be done pretty concretely. According to Definition 1.2.8.1, there is an obvious inclusion $i:C \to C\ast \Delta^0 = \mathcal{C}^{ \triangleright }$. Now you need the retraction.

The key is Proposition 1.2.9.2, which implies that $Hom_{sSet}(C,C/Y) = Hom_p(C\ast \Delta^0,C)$ where $p: \Delta^0 \to C$ has $im(p) = Y$ (here $Hom_p$ means we only want $f: C\ast \Delta^0 \to C$ such that $f|_{\Delta^0} = p$).

Now we have to use what it means to be strongly final. We know that the projection $C/Y \to C$ is a trivial fibration. This means it induces the following equivalence of hom sets $Hom_{sSet}(C,C)\simeq Hom_{sSet}(C,C/Y)$, since every $C \in sSet$ is cofibrant. The identity $id_C$ is taken by the composition $Hom_{sSet}(C,C)\simeq Hom_{sSet}(C,C/Y) = Hom_p(C\ast \Delta^0,C)$ to the desired retraction, $r$. It is an easy and valuable exercise to check that $r\circ i = id_C$. Note the universal property in 1.2.9.2.