Background: Let $S$ be a simplicial set. By freely adding degeneracies to $S$, I mean first applying the forgetfull functor from simplicial sets to semi-simplicial sets which forget the already existing degeneracies maps and then apply its left adjoint which freely add the degeneracies. One gets a new simplicial set $S'$ which can be described explicitly by:
$$ S'_n = \left\lbrace (a,f) |{ a \in S_k \text{ and } f:\{0,\dots,n\} \twoheadrightarrow \{0,\dots,k\} \atop \text{ is an order preserving surjection}}\right\rbrace $$
The simplicial operations being applied to (a,f) as if it was a formal "$f^* a$".
It is know that the canonical map from $S'$ to $S$ (which send $(a,f$) to $f^* a$) is a weak equivalence. Indeed the geometric realization of $S'$ is exactly the same as the "fat geometric realization of $S$" (see def 1 and def 2 in nlab) which is known to be weakly equivalent to the classical geometric realization of $S$.
My question: is it possible to give a purely combinatorial proof of the homotopy equivalence between $S$ and $S'$. The best would be an explicit finite sequence of simplicial homotopy equivalences or trivial Kan fibrations between them.
My motivation is to determine to what extent a result of this kind is likely to be true in more general situations like for example simplicial objects in nice enough combinatorial model categories.
It would also be helpful if someone could point me to a proof that the fat geometric realization is homotopy equivalent to the usual one. I already know two proofs of that in the literature:
The first is in Segal's "Categories and cohomology theories". It deals with the more general case of the geometric realization of a simplicial space, but it just sketches the proof; and once stripped from all the topological consideration not really relevant for my question, it just say something like "it is true when $S$ is $\Delta^n$" (which is already not really trivial I think) and then there is a not completely clear argument to extend this to an arbitrary simplicial set by colimit.
An other one that I have not been able to found back but which was just saying that it is a standard exercise to check that this map induce a bijection on homology and fundamental groups. I haven't check if this exercise is easy or not, but I was hoping for a more explicit proof.
The nLab also mention a "more detailed" proof due to Tammo tom Dieck, but there is no link to it and I couldn't find it on google.
