Given an abstract simplicial complex $K$, one can make a simplicial set $X(K)$ with $n$-simplices given by sequences $(x_0, \ldots, x_n)$ such that $\{x_0, x_1, \ldots, x_n\}$ is a simplex of $K$. The face maps delete entries and the degeneracy maps repeat entries. I'd like a reference for the fact that the geometric realization of $X(K)$ is homotopy equivalent to the geometric realization of $K$ itself. (Note that $|X(K)|$ is typically very big: for $K$ a single edge, $|X(K)|$ is the infinite-dimensional sphere $S^\infty$.)

I've sketched a proof of this fact here, but hope there is a reference I can just cite since, as I expected, every algebraic topologist I've asked in person already knew the fact. :)

Also, does this $X(K)$ have a standard name or notation? Or if not, can someone think of a catchy name or nice notation?

Given an abstract simplicial complex $K$, one can make a simplicial set $X(K)$ with $n$-simplices given by sequences $(x_0, \dotsc, x_n)$ such that $\{x_0, x_1, \dotsc, x_n\}$ is a simplex of $K$. The face maps delete entries and the degeneracy maps repeat entries. I'd like a reference for the fact that the geometric realization of $X(K)$ is homotopy equivalent to the geometric realization of $K$ itself. (Note that $\lvert X(K)\rvert$ is typically very big: for $K$ a single edge, $\lvert X(K)\rvert$ is the infinite-dimensional sphere $S^\infty$.)

I've sketched a proof of this fact at Turning simplicial complexes into simplicial sets, but hope there is a reference I can just cite since, as I expected, every algebraic topologist I've asked in person already knew the fact. :)

Also, does this $X(K)$ have a standard name or notation? Or if not, can someone think of a catchy name or nice notation?