Weak colimits in locally cartesian closed categories The general adjoint functor theorem implies that a complete locally small category has a weak colimit of a diagram if and only if it has a colimit of this diagram. It seems that this is also true for finite colimits in locally cartesian closed categories. For example, if a locally cartesian closed category has a weakly initial object $W$, then we can define the initial object using the internal language:
$$\sum_{x : W} \prod_{f : W \to W} f(x) = x.$$
The proof that this object is initial is similar to the proof of this fact for complete categories. Does this fact about locally cartesian closed categories appears in the literature?
The second question is whether this fact is true for $\infty$-categories. It is true for locally small complete $\infty$-categories as was shown in this paper (Proposition 2.3.2), but I think that it does not hold for locally cartesian closed $\infty$-categories. So, what is an example of a locally cartesian closed $\infty$-category with a weakly initial object, but without the initial one?
UPD: I proved that every weakly initial object in a locally cartesian closed $\infty$-category is initial in my answer, but there is still a more general question: does every locally cartesian closed $\infty$-category with weak finite colimits has finite colimits?
 A: 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.
