Kerodon

Proof. For every topological space $Y$, Example 3.3.2.9 supplies an isomorphism of semisimplicial sets $\operatorname{Sing}_{\bullet }(Y) \rightarrow \operatorname{Ex}( \operatorname{Sing}_{\bullet }(Y) )$. These isomorphisms depend functorially on $Y$, and can therefore be regarded as an isomorphism of functors $G \circ \operatorname{Sing}_{\bullet } \xrightarrow {\sim } G \circ \operatorname{Ex}\circ \operatorname{Sing}_{\bullet }$, where $G: \operatorname{Set_{\Delta }}\rightarrow \operatorname{Fun}( \operatorname{{\bf \Delta }}_{\operatorname{inj}}^{\operatorname{op}}, \operatorname{Set})$ denotes the forgetful functor from simplicial sets to semisimplicial sets. Passing to left adjoints, we conclude that for every semisimplicial set $S_{\bullet }$, we have a canonical homeomorphism $| \operatorname{Sd}( S_{\bullet }^{+} ) | \simeq | S_{\bullet }^{+} |$, depending functorially on $S_{\bullet }$. Proposition 3.3.3.7 now follows from Corollary 3.3.1.11 (applied to the semisimplicial set $X^{\mathrm{nd}}$). $\square$