Homotopy equivalence of simplicial sets

307 Views Asked by At

From Lurie's Kerodon Remark 3.1.6.6 see : https://kerodon.net/tag/00U5.
It is said that a morphism of simplicial set $f : X \rightarrow Y$ is a homotopy equivalence if and only if for every simplicial sets $Z$ composition with $f$ yields a bijection $\pi _0( \operatorname{Fun}(Y_{}, Z_{})) \rightarrow \pi _0( \operatorname{Fun}( X_{}, Z_{}) )$.
We say that $f : X \rightarrow Y$ to be a homotopy equivalence if there exist a morphism of simplicial set $g : Y \rightarrow X$ such that there exists a homotopy $H : \Delta^1 \times X \rightarrow X$ such that $H_{\{0\}\times X} = g \circ f$ and $H_{\{1\}\times X} = \operatorname{id}_X$ and similarly there exists a homotopy $G$ from $g\circ f$ to $\operatorname{id_Y}$.
The implication of the remark is clear since the homotopy inverse of $f$ exhibits an inverse.
However I don't know how to prove the reverse implication namely:
If we suppose that for every simplicial sets $Z$ that $\Theta : \pi _0( \operatorname{Fun}(Y_{}, Z_{})) \rightarrow \pi _0( \operatorname{Fun}( X_{}, Z_{}) )$ is a bijection then in particular it is a bijection for $Z=X$.
Therefore there exists a vertex $g \in \operatorname{Fun}( Y_{}, X_{}) $ identified as a morphism of simplicial set $g : Y \rightarrow X$ such that $g \circ f $ lie in the same connected component of $ \operatorname{id_X}$.
In other words there exists $g\circ f=h_0, \ldots, h_k= \operatorname{id_X}$ a collection of morphism from $X$ to $Y$ such that either there exists a homotopy from $h_i$ to $h_{i+1}$ or a homotopy from $h_{i+1}$ to $h_i$. How can I conclude that there exists a homotopy from $g \circ f$ to $\operatorname{id_x}$ ?
Thanks in advance