Lemma 23.6.5 (Fubini rule for ends). Let \(C\) and \(C'\) be \(\infty \)-categories and let \(F\colon C\catop \times C \times {C'}\catop \times C' \to D\) be a functor. Then there is an equivalence \[ \int _{c \in C} \int _{c' \in C'} F(c,c,c',c') \simeq \int _{(c,c') \in C \times C'} F(c,c,c',c'). \]
Proof. Since a limit over a product category may be computed as an iterated limit, it will suffice to produce an equivalence \[ \Tw (C \times C') \simeq \Tw (C) \times \Tw (C') \] of left fibrations over \(C\catop \times C \times {C'}\catop \times C'\). By straightening-unstraightening, it will suffice to produce a natural isomorphism between their unstraightenings: \[ (x,y,x',y') \quad \mapsto \quad \Hom _{C \times C'}((x,x'), (y,y')) \simeq \Hom _C(x,y) \times \Hom _{C'}(x',y'). \] Unwinding the definition of the hom functors, this boils down to the canonical equivalence \[ \Ar (C \times C') \iso \Ar (C) \times \Ar (C') \] over \(C \times C \times C' \times C'\), coming from the fact that \(\Ar (-) = \Fun ([1],-)\) preserves products. □
Generated from the authoritative LaTeX source.