This is a partial answer that summarizes the discussion in the comments.

It doesn't seem that this fact appears in the literature, but it easily follows from the general adjoint functor theorem for indexed categories applied to locally cartesian closed category with its canonical indexing over itself as Mike Shulman noted.

Now, let us discuss the $\infty$ case. First, let us note that it is not clear how complete indexed $\infty$-categories should be defined: as indexed $\infty$-categories with small products and finite limits or the ones with all small limits. It seems that the latter condition is stronger than the former in general. It is not clear if locally cartesian closed $\infty$-categories satisfy the latter condition, but it seems that they do satisfy the former. Anyway, can we prove the general adjoint functor theorem for indexed $\infty$-categories using either of the definitions of completeness? I don't know if the stronger condition can be used to prove it, but it seems that the weaker one alone is not enough. Nevertheless, I believe that it is enough if we assume additionally that the base $\infty$-category is idempotent complete. We cannot apply this fact to locally cartesian closed $\infty$-categories since they are not idempotent complete in general.

So, it seems that we cannot use the general adjoint functor theorem for indexed $\infty$-categories to prove this fact for locally cartesian closed $\infty$-categories. Nevertheless, we can prove directly that a weakly initial object in a locally cartesian closed $\infty$-category is initial. I will use the internal language (that is, HoTT with identity types, $\Sigma$-types, and extensional $\Pi$-types) to prove this. If $W$ is weakly initial, then it is a proposition (that is, a subterminal object). This follows from the fact that we have a map $W \to \mathrm{isProp}(W)$, where $\mathrm{isProp}(W) = \prod_{(x,y : W)} x = y$. This implies that every map $D \to W$ has a section, which implies that $W$ is initial. Indeed, if we consider $D = \sum_{(x : W)} f(x) = g(x)$, then a section of the obvious projection $D \to W$ proves that $f = g$. Note that this is a proof in the internal language, so this indeed proves that the space $\mathrm{Hom}(W,X)$ is contractible and not just that it is connected.

This answers the question in the original post, but I don't know if this argument can be applied to other weak finite colimits. The problem is that every weakly initial object is initial in a locally cartesian closed $\infty$-category, but this is not true for other weak colimits. I updated the post to include this more general question.

7more comments