I have a question about a proof from Jacob Lurie's [Higher Topos Theory](https://people.math.harvard.edu/%7Elurie/papers/highertopoi.pdf) (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?



Strongly final vertex $Y$ in a simplicial set gives a retraction of $\mathcal{C}^{ \triangleright }$ onto $\mathcal{C}$
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.


