Dependent-product-preserving morphisms are closed under limits

Let \(T_{\bullet}\colon I\to\Logos\) be a diagram whose transition morphisms preserve dependent products, and let \(T:=\lim_iT_i\). By Proposition 4.30, the underlying category of \(T\) is the limit of the categories \(T_i\). Slices, pullback functors, and their right adjoints are therefore computed pointwise. Hence every projection \(T\to T_i\) preserves dependent products. The same pointwise description shows that the universal cone remains a limit cone in the wide subcategory, which proves the claim.