Homotopic quotients of simplicial sets as infinity-groupoids Suppose $f:X \to Y$ is a function of sets. Then we can take the quotient $X/\text{~}$ by identifying $x \text{~} y$ if and only if $f(x)=f(y)$. Now suppose instead that $f:X \to Y$ is a map of simplicial sets. I want to emulate this homotopically, by adding a 1-simplex between $x$ and $y$ if there is a 1-simplex from $f(x)$ to $f(y)$, (and similarly on higher simplices). This is probably most clear if you think of $X$ and $Y$ as infinity groupoids (as indeed I have in mind). I want a way of "making guys equivalent if they're equivalent after applying f". So, if $X$ and $Y$ are Kan, adding a 1-simplex between two 0-simplices makes them "weakly isomorphic" (which is the correct thing to do, not just glue them together outright). Is there a standard construction for maps of (maybe Kan?) simplicial sets that does this?
 A: I'd think the construction in question is the homotopy coimage of $f$ (it's unfortunately called "coimage" even though it behaves like the image).
First one forms the homotopy Cech nerve
$$  
    C(f) = 
    \left(
     \cdots X \times_Y X \times_Y X \stackrel{\longrightarrow}{\stackrel{\longrightarrow}{\longrightarrow}}X  \times_Y X \stackrel{\longrightarrow}{\longrightarrow} X
   \right)
$$
This is the internal groupoid object that encodes the $\infty$-equivalence relation on the elements of $X$  "is equivalent in $Y$"
Forming its homotopy colimit
$$
  coim(f) := \lim_{\to} C(f)
$$
produces the homotopy quotient of $X$ by this equivlence relation.
As an example, take $\mathbf{B}G$ the one-object groupoid of a group $G$ and $* \to \mathbf{B}G$ the point inclusion. One wants to see that the homotopy image of the point inclusion $* \to \mathbf{B}G$ is not just the point, but is $*//G$, i.e. $\mathbf{B}G$ itself, because there is $G$ worth of ways for the point to be equivalent to itself after inclusion into $\mathbf{B}G$.
So one computes the homotopy Cech nerve and finds the familiar
$$
  C(* \to \mathbf{B}G) =
  \left(  
     \cdots G \times G \times G \stackrel{\longrightarrow}{\stackrel{\longrightarrow}{\stackrel{\longrightarrow}{\longrightarrow}}} G\times G \stackrel{\longrightarrow}{\stackrel{\longrightarrow}{\longrightarrow}} G \stackrel{\longrightarrow}{\longrightarrow} \ast
  \right)
$$
but now regarded as a simplicial object in $\infty Grpd$. This is the diagram that encodes the action of $G$ on the point. Its homotopy colimit is indeed again $\mathbf{B}G$, so that we find
$$
  coim(* \to \mathbf{B}G) = \mathbf{B}G
$$
That this comes out this way is an example of Giraud's axioms at work, since $\infty Grpd$ happens to be an $\infty$-topos: this implies that every $\infty$-groupoid object (simplicial diagram as above) in $\infty Grpd$ is effective .
A: You are looking at the coequaliser of the kernel pair, so my guess would be to take the homotopy pullback of $f$ along itself, then look at the nerve of the groupoid $X\times_Y X \rightrightarrows X$ in $sSet$ this gives rise to, then form the diagonal (=hocolim) of this bisimplicial set. I guess this comes with a map to $Y$, but I haven't checked.
A: This answer is perhaps a gloss on David's one. It is often useful to replace taking a quotient by forming the equivalence relation as a groupoid. Thus the initial situation you describe has the classical equivalence-relation-from-a-function form.  This will work in any category with pullbacks as it is the pullback of f along itself. In a homotopy situation, such as you need, the analogue will be the homotopy pullback of $f$ along itself.
This does not form the quotient as such, but is, I maintain, better (especially in the presence of differential structures for instance).It corresponds to the idea that was sketched in the question, but is natural functorial and so less hassle(<- technical categorical term meaning 'less hassle'!). It is also going to give results that do not depend on the homotopy class of $f$ and that is often important especially if you are thinking of the simplicial sets as being weak infinity groupoids or similar. I believe there are extensions to quasicomplexes but do not have sources with me to check at the moment or to give chapter and verse. 
This construction not only says two simplices in $Y$ are to be thought of as being the same but records WHY, and that is important.
(Edit: Thanks Tom.  I should have said 'It is also going to give results that only depend on the homotopy class of $f$ ..')
A: You might like to look at the 1978 thesis of Nick Ashley on "Simplicial $T$-complexes and crossed complexes: a 
  nonabelian version of a theorem of Dold and Kan." available from Esquisses Math. 1978 at http://ehres.pagesperso-orange.fr/Cahiers/Ctgdc.htm
He considers a filtered Kan complex $K_* $  and a natural homotopy relation to give a Kan fibration $p: K_*  \to \rho(K_* )$, where $\rho(K_*)$ is a simplicial $T$-complex, i.e. a strong form of Kan complex with unique "thin" fillers. Modifications of this should give you strict consructions of the kind you want. 
