Universal property trivial operad

Proof. Let us first check that \(\Triv _C\) is an \(\infty \)-operad. By Construction 14.1.16, the \(\infty \)-category \(\Fin (C\catop )\) admits finite coproducts and \(q\) preserves them, so \(\Triv _C^{\otimes } = \Fin (C\catop )\catop \) admits finite products and \(q\catop \) preserves them; as the inclusion \(\Fin \catop \hookrightarrow \Span (\Fin )\) preserves finite products by part (1) of Lemma 13.3.8, the same is true for \(p_{\Triv _C}\). Since the products of \(\Triv _C^{\otimes }\) are the concatenations of tuples, the fiber over a finite set \(I\) is \(C^I\), whose decomposition \(C^I \simeq \prod _{i \in I}C\) is the one required in the definition of an \(\infty \)-operad.

For the final condition, consider objects \(X_i = \{x^i_a\}_{a \in A_i}\) of \(\Triv _C^{\otimes }\) for \(i \in I\) and a map \(f\colon J \to I\) of finite sets. Read in \(\Fin (C\catop )\), the morphism \(\widetilde {f}\colon \prod _{i \in I}X_i \to \prod _{j \in J}X_{f(j)}\) is the map \(\coprod _{j \in J}X_{f(j)} \to \coprod _{i \in I}X_i\) which restricts on the \(j\)-th summand to the inclusion of \(X_{f(j)}\); it lies over the map \(\bigsqcup _{j \in J}A_{f(j)} \to \bigsqcup _{i \in I}A_i\), \((j,a) \mapsto (f(j),a)\), and all of its components in \(C\catop \) are identities. It is therefore \(q\)-cartesian, and hence \(\widetilde {f}\) is \(q\catop \)-cocartesian. It remains \(p_{\Triv _C}\)-cocartesian after composing with the inclusion \(\Fin \catop \hookrightarrow \Span (\Fin )\): every morphism of \(\Triv _C^{\otimes }\) lies over a backwards span, and composing a non-backwards span with a backwards span is again non-backwards, so the mapping animae over the remaining spans are empty on both sides.

The description of the multimorphism animae follows: the active span \(I \xleftarrow {=} I \to \lra {1}\) lies in \(\Fin \catop \) only when \(I\) is a singleton, in which case it is the identity of \(\lra {1}\). Thus \(\Triv _C(\{x_i\}_{i \in I};y)\) is empty unless \(I = \{i_0\}\), in which case it is the anima of morphisms \(x_{i_0} \to y\) in the fiber \((\Triv _C)_{\lra {1}} \simeq C\).

We turn to the universal property, which will follow from the universal property of \(\Fin (C\catop )\). Indeed, applying Lemma 14.1.17 to \(C\catop \) and passing to opposite categories, we see that restriction along the inclusion \(j\colon C \hookrightarrow \Triv _C^{\otimes }\) of the fiber over \(\lra {1}\) induces an equivalence \[ j^*\colon \Fun ^{\times }(\Triv _C^{\otimes },E) \iso \Fun (C,E) \] for every \(\infty \)-category \(E\) that admits finite products. This equivalence is natural in \(E\), so applying it to \(E = \Oo ^{\otimes }\) and to \(E = \Span (\Fin )\) yields a commutative square

The composite \(p_{\Triv _C} \circ j\) is the constant functor at \(\lra {1}\), so passing to the fibers over \(p_{\Triv _C}\) and \(\const _{\lra {1}}\) gives equivalences \[ \Fun _{\Op _{\infty }}(\Triv _C,\Oo ) \iso \Fun (C,\Oo ^{\otimes })\times _{\Fun (C,\Span (\Fin ))}\{\const _{\lra {1}}\} \simeq \Fun (C,\Oo _{\lra {1}}), \] where the second equivalence holds because \(\Fun (C,-)\) preserves pullbacks. By construction, this equivalence is given by restriction to the underlying \(\infty \)-categories. □