Cocartesian transport symmetric monoidal componentwise

Observation 14.2.7. Cocartesian transport in \(C^{\otimes }\) is compatible with finite products. More precisely, suppose that \(\alpha _j\colon I_j\to J_j\) are morphisms in \(\Span (\Fin )\) and that \(\phi _j\colon X_j\to Y_j\) are \(p_C\)-cocartesian lifts of \(\alpha _j\). Since the straightening of \(p_C\) preserves finite products, the product \[ \prod _j\phi _j\colon \prod _jX_j\longrightarrow \prod _jY_j \] is a \(p_C\)-cocartesian lift of the product \(\prod _j\alpha _j\). In particular, cocartesian transport along a forward span is computed separately over the elements of its target.