Lemma 15.3.8. The subcategory \(C^{\times }_{\mathrm {con}}\subseteq \widetilde C^{\times }\) is closed under cocartesian transport. In particular, \(C^{\times }_{\mathrm {con}}\to \Span (\Fin )\) is a cocartesian fibration.
Proof. For a span \(I\xleftarrow {f}K\xrightarrow {g}J\), the functor \(f_!g^*\colon \Fin _{/J}\to \Fin _{/I}\) preserves finite coproducts: pullback along \(g\) does so because \(\Fin \) is extensive, while postcomposition along \(f\) plainly does so. Hence \((f_!g^*)\catop \) preserves finite products, and restriction along it preserves finite-product-preserving functors. □
Generated from the authoritative LaTeX source.