It is well known that any homotopy type can be obtained as the classifying space of a ($1$-)category. The classifying space of a category $\mathcal{C}$ can be interpreted in at least two ways:

  1. We can view $\mathcal{C}$ as an object in the $(\infty,1)$-category of $(\infty,1)$-categories, and localise $\mathcal{C}$ along all its morphisms.
  2. We can consider the constant functor $\mathcal{C} \to \mathbf{Type}, \; X \mapsto *$ (where $\mathbf{Type}$ denotes the $(\infty,1)$-category of homotopy types), and take its colimit. (Or thus equivalently the free homotopy colimit of the unique functor $\mathcal{C} \to 1$, where $1$ denotes the category with only one morphism; see Dugger).

Using various models these two views as well as their equivalence can be made precise as follows: View $\mathcal{C}$ as an object in $\mathbf{SSet}$ equipped with the Joyal model structure. Inverting all morphisms of $\mathcal{C}$ just corresponds to taking its fibrant replacement in the Kan model structure. Taking the colimit in 2. can be formalised by taking the geometric realisation of (the nerve of) $\mathcal{C}$: This is exactly the formula you get for computing the homotopy colimit of the constant functor $\mathcal{C} \to \mathbf{Top}, \; X \to *$ using the simplicial replacement of this functor (described e.g. here).

My question then is:

Is there a model independent way of seeing that these two constructions are equivalent?

So I'm looking for an argument which could be formalised in any model of $(\infty,1)$-categories.

  • 1
    $\begingroup$ A quick observation: by Yoneda this is equivalent to $\lim_C X = \mathrm{Map}(C,X)$. Proving this is very easy if you have at your disposal the theory of (co)cartesian fibrations, but of course this is not model independent. $\endgroup$ Nov 10, 2016 at 21:23

1 Answer 1


Here is an argument, which is basically Denis Nardin's comment.

To have a model independent proof you need model independent definitions of the hocolim and of the localization. You can define them via adjunctions, but from a pragmatic point of view I am not sure this is so helpful. Ultimately to do any kind of calculation you will have to pick a model and a construction of the localization/hocolim and if your definition is the model independent one, then you have the additional task of proving that they satisfy these definitions.


There is an ($\infty$-)adjuction of $(\infty,1)$-categories: $$hocolim_C : Cat_{(\infty,0)}^C \leftrightarrows Cat_{(\infty,0)}: const$$ and this is a definition $hocolim_C$. Here $Cat_{(\infty,0)} \simeq Top$ is the usual $(\infty,1)$-category of spaces which the OP called Type.

There is another one: $$ ||-||: Cat_{(\infty,1)} \leftrightarrows Cat_{(\infty,0)}: i $$ which defines the localization at all morphisms $||C||$. Here $i$ is the inclusion of $(\infty,0)$-cats (= spaces) into all $(\infty,1)$-categories.

Then this means that for all spaces $X$ we have $$ \begin{align} Cat_{(\infty,0)}( hocolim_C const(*) , X) &\simeq Cat_{(\infty,0)}^C( const(*), const(X)) \\ &\simeq Fun(C, Cat_{(\infty,0)}(*, X)) \\ &\simeq Fun( C, iX) \\ & \simeq Cat_{(\infty,0)}( ||C||, X) \end{align} $$

And so by Yoneda you conclude that $hocolim_C const(*) \simeq ||C||$.

  • $\begingroup$ Huh, this was much more straightforward than I thought. Thanks for the detailed answer! $\endgroup$ Nov 10, 2016 at 22:26
  • $\begingroup$ Using $Top$ is a bit weird for what is a model-independent argument. Why not $\mathcal{S}$ ('spaces') or $\infty Gpd$ or the like? $\endgroup$ Nov 11, 2016 at 0:56
  • 1
    $\begingroup$ @DavidRoberts That is a fair point. I edited to use $Cat_{(\infty,0)}$. $\endgroup$ Nov 11, 2016 at 13:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.