Binary products of families

Let \(u_1\colon E_1 \to B_1\) and \(u_2\colon E_2 \to B_2\) be families. For an object \(X \to B_1 \times B_2\), write \(f_i\colon X \to B_i\) for the two projections. Consider the presheaf on \(T_{/B_1 \times B_2}\) which sends \(X\) to the anima of isomorphisms in \(T_{/X}\) between the pullbacks of \(u_1\) and \(u_2\) to \(X\). This presheaf preserves limits: if \(X \simeq \colim_i X_i\) in \(T_{/B_1 \times B_2}\), then descent identifies \(T_{/X}\) with \(\lim_i T_{/X_i}\), and under this identification the two pulled-back families are the compatible systems of their pullbacks to the \(X_i\). Thus isomorphisms between them are computed as the limit of the isomorphism animae over the \(X_i\). By the adjoint functor theorem, the presheaf is therefore representable by some object \(P \to B_1 \times B_2\). Pulling back either \(u_1\) or \(u_2\) along the universal isomorphism gives a family over \(P\), and this family is the product \(u_1 \times u_2\) in \(\Fam(T)\).It remains to prove preservation of colimits in each variable. Fix a family \(u_1\colon E_1 \to B_1\). To show that \(u_1 \times -\colon \Fam(T) \to \Fam(T)\) preserves colimits, we may equivalently show that for any family \(v\colon E' \to B'\) the functor induced by \(u_1 \times -\) preserves colimits, since slices detect colimits. Let \(P'\) denote the base of the product \(u_1\times v\). We claim that under the equivalences \(\Fam(T)_{/v} \simeq T_{/B'}\) and \(\Fam(T)_{/u_1\times v} \simeq T_{/P'}\) from Lemma 4.43, the functor identifies with pullback along the projection map \(P' \to B'\). Since this functor preserves colimits by descent in \(T\), this will finish the proof. To show the claim, we must show that for every \(f\colon u_2 \to v\) in \(\Fam(T)\) with base \(f_B\colon B_2 \to B'\), the square of bases

is a pullback square in \(T\). We compare the presheaves represented by the two objects over \(B_1\times B_2\). Let \(X\to B_1\times B_2\) be an object, and write \(g_1\colon X\to B_1\) and \(g_2\colon X\to B_2\) for the two projections. The object \(P\) represents the presheaf On the other hand, the pullback \((B_1\times B_2)\times_{B_1\times B'}P'\) represents the presheaf because \(P'\) represents the analogous equivalence presheaf for \(u_1\) and \(v\) over \(B_1\times B'\). Since \(f\colon u_2\to v\) is a morphism in \(\Fam(T)\), the family \(u_2\) is the pullback \(f_B^*v\), and hence \(g_2^*u_2\simeq (f_Bg_2)^*v\). These two presheaves are therefore naturally equivalent, proving that the square is a pullback.