Proposition 15.3.10. There is a canonical equivalence over \(\Span (\Fin )\) between the concrete model \(C^{\times }_{\mathrm {con}}\) and the total category \(C^{\times }\) of the cartesian monoidal structure.
Proof. By the uniqueness of cartesian monoidal structures from Proposition 15.3.6, it suffices to show that \(C^{\times }_{\mathrm {con}}\) defines a cartesian monoidal structure on \(C\).
By Lemma 15.3.8, the projection \(C^{\times }_{\mathrm {con}}\to \Span (\Fin )\) is a cocartesian fibration. Under the fiber equivalences of Lemma 15.3.9, the product-comparison maps of its straightening are the canonical equivalences \[ C^{I\sqcup J}\simeq C^I\times C^J, \] and its value at \(\emptyset \) is the terminal category. Thus the straightening preserves finite products, so Lemma 14.2.4 makes \(C^{\times }_{\mathrm {con}}\) into a symmetric monoidal \(\infty \)-category with underlying \(\infty \)-category \(C\).
Transport along a span \(I\xleftarrow {f}K\xrightarrow {g}J\) sends an \(I\)-indexed family to \[ (x_i)_{i\in I}\longmapsto \left (\prod _{k\in g^{-1}(j)}x_{f(k)}\right )_{j\in J}. \] Hence its unit is terminal, its binary tensor product is the product in \(C\), and its inert structure maps are the product projections. By Lemma 15.3.4, it is therefore cartesian monoidal. □
Generated from the authoritative LaTeX source.