The cocartesian operad is an ∞-operad

Proof. We have already argued that \(C^{\amalg } = \Span _{\ct ,\all }(\Fin (C))\) has finite products and that \(p_C^{\amalg } = \Span (q)\) preserves them, giving condition (1) of the definition. The objects in the fiber over a finite set \(I\) form the fiber \(\Fin (C)_I=C^I\). Moreover, by Lemma 13.1.13, a morphism over the identity span of \(I\) is represented by a span whose backwards leg is \(q\)-cartesian over \(\id _I\), hence an isomorphism, and therefore reduces to a morphism in \(C^I\). Thus the fiber of \(C^{\amalg }\) over \(I\) is \(C^I\), giving condition (2). For condition (3), consider objects \(X_i \in \Fin (C)\) and a morphism \(f\colon J \to I\) of finite sets. Then the lift \(\widetilde {f}\colon \prod _{i \in I} X_i \to \prod _{j \in J} X_{f(j)}\) in \(\Span _{\ct ,\all }(\Fin (C))\) is a backwards span of the form \[ \bigsqcup _{i \in I} X_i \xleftarrow {(f,(\id )_j)} \bigsqcup _{j \in J} X_{f(j)} \xrightarrow {(\id ,(\id ))} \bigsqcup _{j \in J} X_{f(j)}. \] The left-pointing morphism is \(q\)-cartesian and the right-pointing morphism is an identity. In particular, condition (4) of Theorem 15.1.7 only asks for cocartesian lifts of base changes of an identity, which are again isomorphisms; the remaining conditions follow directly from cartesianness and Lemma 15.1.8. Hence this span is \(\Span (q)\)-cocartesian, as desired. □