# Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$

Theorem 3.3.5.1. Let $X$ be a simplicial set. Then the comparison map $\rho _{X}: X \rightarrow \operatorname{Ex}(X)$ of Construction 3.3.4.3 is a weak homotopy equivalence.

Proof of Theorem 3.3.5.1. Let $X$ be a simplicial set. We wish to prove that the comparison map $\rho _{X}: X \rightarrow \operatorname{Ex}(X)$ is a weak homotopy equivalence. Fix a Kan complex $Y$; we must show that composition with $\rho _{X}$ induces a bijection $\pi _0( \operatorname{Fun}( \operatorname{Ex}(X), Y) ) \rightarrow \pi _0( \operatorname{Fun}(X,Y) )$. This map fits into a diagram

$\xymatrix@R =50pt@C=50pt{ \pi _0( \operatorname{Fun}( \operatorname{Ex}(X), Y) ) \ar [r]^-{ \circ \rho _ X} \ar [d]^{ \rho _{Y} \circ }_{\sim } & \pi _0( \operatorname{Fun}(X,Y) ) \ar [d]^{ \rho _{Y} \circ }_{\sim } \ar [dl]_{f \mapsto \operatorname{Ex}(f)} \\ \pi _0( \operatorname{Fun}(\operatorname{Ex}(X), \operatorname{Ex}(Y) )) \ar [r]^-{ \circ \rho _{X} } & \pi _0( \operatorname{Fun}(X, \operatorname{Ex}(Y)) ),}$

where the vertical maps are bijective (Proposition 3.3.5.7) and the lower triangle commutes by the naturality of $\rho$. To show that the upper horizontal map is bijective, it will suffice to show that the upper triangle also commutes. Fix a map $f: \operatorname{Ex}(X) \rightarrow Y$. We then compute

$\operatorname{Ex}(f \circ \rho _{X} ) = \operatorname{Ex}(f) \circ \operatorname{Ex}(\rho _{X}) \sim \operatorname{Ex}(f) \circ \rho _{\operatorname{Ex}(X)} = \rho _{Y} \circ f$

where the equality on the left follows from functoriality, the equality on the right from the naturality of $\rho$, and the homotopy in the middle is supplied by Proposition 3.3.5.8. $\square$