Limit projections are étale

Let \(D:=\prod_{i\in I} C_i\). By Lemma 4.58, it suffices to prove that the forgetful morphism is an étale morphism. By Proposition 4.56, it is enough to show that \(\pi\) preserves dependent products and provides enough univalent families.Every étale morphism preserves dependent products by Proposition 4.37 and Lemma 4.52. Hence Proposition 4.50 shows that \(\pi\) preserves dependent products.Let \(u=(u_i)_{i\in I}\) be a univalent family in \(D\), i.e. a tuple of univalent families \(u_i\in \Fam^{\univ}(C_i)\) without imposing the transition equivalences. Since limits of logoi are computed in \(\Cat\), we have \(\Fam(C_{-\infty})\simeq \lim_i\Fam(C_i)\). Hence \(\Fam^{\univ}(C_{-\infty})\) is the full subposet of \(\Fam^{\univ}(D)\) spanned by the tuples equipped with equivalences \(s^*(u_i)\simeq u_j\) for all arrows \(s\colon i\to j\) in \(I\); the higher coherences are automatic because univalent families form a poset. We will enlarge \(u\) to such a compatible tuple.For a morphism \(s\colon i\to j\) in \(I\), write \(s^*\colon C_i\to C_j\) for the corresponding étale morphism of logoi, and write \(s_{\sharp}\colon C_j\to C_i\) for its left adjoint. Both functors induce functors on families. For \(s^*\) this follows from left exactness. For \(s_{\sharp}\) it follows from the indexed condition in Lemma 4.52; after identifying \(s^*\) with a pullback functor into a slice, \(s_{\sharp}\) is the total-object functor and therefore preserves pullback squares. Both induced functors preserve colimits of families: \(s^*\) preserves colimits as a morphism of logoi, while \(s_{\sharp}\) preserves them as a left adjoint, and colimits in \(\Fam(C_i)\) and \(\Fam(C_j)\) are computed in the corresponding arrow categories by Lemma 4.44.Define an endofunctor \(\Phi\) of \(\Fam(D)\) by Let \(G\) be the endofunctor of \(\Fam^{\univ}(D)\) obtained by applying univalent completion componentwise to \(\Phi\). The summands indexed by the identity morphisms give a natural map \(u\to G(u)\). Moreover, for every \(s\colon i\to j\) there are natural maps the second obtained by adjunction from \(s_{\sharp}(u_j)\to G(u)_i\).Now form the chain and set \(u^{\infty}:=\colim_n G^n(u)\). This colimit is computed in \(\Fam(D)\) and remains univalent by Corollary 4.46. The functor \(G\) preserves sequential colimits: the functor \(\Phi\) does so by the preceding paragraph, and univalent completion does so because it is a left adjoint. Consequently, Here it is essential that univalent families form a poset. In particular, the two morphisms \(G(u)\to G^2(u)\) obtained by applying \(G\) to \(u\to G(u)\) and by evaluating the natural transformation \(\id\to G\) at \(G(u)\) agree, and all higher compatibilities are unique. Thus applying \(G\) to the displayed chain gives its tail. Under the resulting identification, the natural map agrees with the map induced by the structure maps \(G^n(u)\to G^{n+1}(u)\). It is an isomorphism because the inclusion of the tail of \([\omega]\) is final. This is the usual Adámek fixed-point argument [Adamek 1974].For every arrow \(s\colon i\to j\), the displayed maps for \(G\) pass to the colimit and give morphisms between univalent families. Here the fixed-point equivalence identifies the shifted colimits appearing in the construction with \(u^{\infty}\). Since univalent families form a poset inside \(\Fam(C_j)\), these two maps exhibit \(s^*(u^{\infty}_i)\) and \(u^{\infty}_j\) as equivalent. The higher compatibility data are unique for the same reason. Thus \(u^{\infty}\) is a univalent family in the limit logos \(C_{-\infty}\), and the map \(u\to u^{\infty}\) shows that \(\pi\) provides enough univalent families.