Understanding model independently the equivalence of two ways of obtaining homotopy types from categories

Question

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.

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.

Anyway...

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||$.