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?
