Monoidal transport along simplicial thickenings

Proof. The projection \(X\times \abs {\Delta ^q}\to X\) is a homotopy equivalence, so \(p_{X,q}\) is an isomorphism of animae. Consequently, restriction along \(p_{X,q}\) is a symmetric monoidal equivalence \[ p_{X,q}^*\colon \Fun (\Pi _{\infty }(X),\An _*) \longrightarrow \Fun (\Pi _{\infty }(X\times \abs {\Delta ^q}),\An _*). \] Its inverse \((p_{X,q})_!\) inherits the unique symmetric monoidal structure of an inverse equivalence. It follows that \(\Phi _{X,q}\) is symmetric monoidal.

A morphism \(\alpha \colon [m]\to [q]\) in \(\simp \) induces a commutative square

where \(\bar \alpha \) is the corresponding affine map. All three induced maps of fundamental animae in this square are isomorphisms. The natural transformation of Lemma 10.5.6, together with functoriality of the inverse equivalences given by left Kan extension, therefore gives a symmetric monoidal natural isomorphism \[ \Phi _{X,m}\circ (\id _X\times \bar \alpha )^* \cong \Phi _{X,q}. \] These isomorphisms are compatible with composition because both the naturality of \(\xi \) and left Kan extension are functorial. They therefore define the asserted cocone. For a continuous map \(f\colon Y\to X\), the analogous commutative square has the projections to \(Y\) and \(X\) as its vertical maps. Since these induce isomorphisms of fundamental animae, the same argument gives a symmetric monoidal natural isomorphism \[ \Phi _{Y,q}\circ (f\times \id _{\abs {\Delta ^q}})^* \cong (\Pi _{\infty }f)^*\circ \Phi _{X,q}. \] The coherence of these isomorphisms under composition follows from the same functoriality, proving that the cocone is natural in \(X\). □