Hinich Winges model Day

Proof. Let us write \(\Dd \) for this pullback. We will show directly that \(\Dd \) satisfies the defining universal property of \(\oDay (\Mm _C,\Mm _D)\). It will suffice to produce for any \(\infty \)-operad \(\Pp \) a natural equivalence \[ \Fun _{\Op _{\infty }}(\Pp ,\Dd ) \simeq \Fun _{\Op _{\infty }}(\Pp \times \Mm _C, \Mm _D). \] For the left-hand side, note that \(\Fun _{\Op _{\infty }}(\Pp ,-)\) commutes with pullbacks. Since \(\Comm \) is the terminal \(\infty \)-operad, we have \(\Fun _{\Op _{\infty }}(\Pp ,\Comm ) \simeq *\). Since operad morphisms from \(\Pp \) into a cartesian operad correspond to \(\Pp \)-monoids by Theorem 15.3.11, we obtain equivalences \[ \hspace {-5pt} \Fun _{\Op _{\infty }}(\Pp ,\OpCart _{\Ar ^{\oplax }}) \simeq \Mon _{\Pp }(\Ar ^{\oplax }), \qquad \Fun _{\Op _{\infty }}(\Pp ,\OpCart _{\Cat _{\infty } \times \Cat _{\infty }}) \simeq \Mon _{\Pp }(\Cat _{\infty } \times \Cat _{\infty }). \] It follows that the \(\infty \)-category \(\Fun _{\Op _{\infty }}(\Pp ,\Dd )\) is equivalent to the fiber of the map \[ \Mon _{\Pp }(\Ar ^{\oplax }) \to \Mon _{\Pp }(\Cat _{\infty }) \times \Mon _{\Pp }(\Cat _{\infty }) \] over the pair \((C_{\Pp },D_{\Pp })\), where \(C_{\Pp }\) and \(D_{\Pp }\) are obtained from \(C\) and \(D\) by precomposition with the operad map \(p_{\Pp }\colon \Pp \to \Comm \). By Theorem 16.2.2, this fiber is the \(\infty \)-category \(\Fun ^{\Pp \dlax }(C_{\Pp },D_{\Pp }) = \Fun _{(\Op _{\infty })_{/\Pp }}(\Mm _{C_{\Pp }/\Pp }, \Mm _{D_{\Pp }/\Pp })\) of lax \(\Pp \)-monoidal functors \(C_{\Pp } \to D_{\Pp }\). By the definition of \(C_{\Pp }\) and \(D_{\Pp }\) we have \[ \Mm _{C_{\Pp }/\Pp } \simeq \Pp \times _{\Comm } \Mm _C \qquadtext { and } \Mm _{D_{\Pp }/\Pp } \simeq \Pp \times _{\Comm } \Mm _D, \] hence \[ \hspace {-6pt} \Fun _{(\Op _{\infty })_{/\Pp }}(\Mm _{C_{\Pp }/\Pp }, \Mm _{D_{\Pp }/\Pp }) \simeq \Fun _{(\Op _{\infty })_{/\Pp }}(\Pp \times _{\Comm } \Mm _C, \Pp \times _{\Comm } \Mm _D) \simeq \Fun _{\Op _{\infty }}(\Pp \times _{\Comm } \Mm _C, \Mm _D), \] where the second equivalence uses the universal property of pullbacks. Since \(\Comm \) is terminal, the fiber product \(\Pp \times _{\Comm }\Mm _C\) is the product \(\Pp \times \Mm _C\) in \(\Op _{\infty }\). This was precisely what we wanted to show. □