Cocartesian monoidal structure map

Construction 15.2.10. Let \(C\) be an \(\infty \)-category. We construct a functor \[ \iota \colon \Span (\Fin ) \times C \to C^{\amalg } = \Span _{\ct ,\all }(\Fin (C)), \] informally given by sending a pair \((I,x)\) to the ‘constant’ \(I\)-tuple \((x)_{i \in I}\), and by sending a pair \((I \xleftarrow {f} J \xrightarrow {g} K, \phi \colon x \to y)\) of a span in \(\Fin \) and a morphism in \(C\) to the span \[ (x)_{i \in I} \xleftarrow {(f,(\id _x)_{j \in J})} (x)_{j \in J} \xrightarrow {(g,(\phi )_{j \in J})} (y)_{k \in K}. \] (Note that the left-pointing morphism is indeed \(q\)-cartesian.) Formally, this map is constructed as follows:

• Consider the natural transformation \(\Delta \colon \const _C \to C^{(-)}\) of functors \(\Fin \catop \to \Cat _{\infty }\) which on the one-point set is given by the identity \(\id _C\colon C \to C\); this property determines the entire transformation since \(C^{(-)}\) is by definition right Kan extended from the point. For a finite set \(I\), it is given by the diagonal functor \[ \Delta \colon C \to C^I, \quad x \mapsto (x)_{i \in I}. \]
• By cartesian unstraightening, we obtain a morphism of cartesian fibrations over \(\Fin \):

  

• By using Proposition 15.1.9, both sides become adequate triples with left class given by the cartesian morphisms. The functor \(\Un ^{\ct }(\Delta )\) preserves cartesian morphisms and becomes a morphism of adequate triples. Since a morphism on the left-hand side is cartesian if and only if the \(C\)-component is an isomorphism, we may use the equivalence \(\Span _{\simeq ,\all }(C) \simeq C\) to get a map on spans: