Product with trivial operad

Proof. Recall that \(\Triv ^{\otimes } = \Fin \catop \) and that \(p_{\Triv }\colon \Fin \catop \hookrightarrow \Span (\Fin )\) is the inclusion. The product operad \(\Triv \times \Oo \) is therefore represented by the pullback

By the defining properties of an \(\infty \)-operad, the left vertical map is a cocartesian fibration whose cocartesian straightening preserves finite products and sends \(\lra {1}\) to \(\Oo _{\lra {1}}\). It is therefore equivalent to \[ \Fin \catop \to \Cat _{\infty }, \qquad I \mapsto \Oo _{\lra {1}}^I. \] By Remark 14.1.19, its cocartesian unstraightening is precisely \[ q_{\Oo _{\lra {1}}}\catop \colon \Fin (\Oo _{\lra {1}}\catop )\catop \to \Fin \catop , \] which is the total category of \(\Triv _{\Oo _{\lra {1}}}\). □