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

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?

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.
• Alright I see, the key is then that trivial fibration implies especially that we can lift $id:C \to C$ to $C/Y$ and then we use the adjunction from 9.2 ... Thank you a lot! Commented Aug 30, 2022 at 12:32