Direct construction of the cartesian operad

Construction 15.3.7. The target projection \(\ev _1\colon \Ar (\Fin )\to \Fin \) is a cartesian fibration whose cartesian straightening sends \(I\) to \(\Fin _{/I}\). Thus pullback defines a functor \(\Fin \catop \to \Cat _{\infty }\) with value \(\Fin _{/I}\) at \(I\). Each pullback functor \(f^*\colon \Fin _{/J}\to \Fin _{/I}\) has a left adjoint \(f_!\), given by postcomposition with \(f\). The Beck–Chevalley isomorphisms follow from the pasting law for pullback squares. Its unfurling therefore sends a span \(I\xleftarrow {f}K\xrightarrow {g}J\) to \(g_!f^*\colon \Fin _{/I}\to \Fin _{/J}\).

Precomposing this unfurling with the leg-swap equivalence \(\Span (\Fin )\simeq \Span (\Fin )\catop \) from Lemma 13.1.15 and then passing to opposites gives a functor \(\Span (\Fin )\catop \to \Cat _{\infty }\). Let \[ r\colon A\to \Span (\Fin ) \] be its cartesian unstraightening. Its fiber over \(I\) is \((\Fin _{/I})\catop \), and its cartesian transport along a span \(I\xleftarrow {f}K\xrightarrow {g}J\) is \((f_!g^*)\catop \).

Applying \(B\mapsto \Fun (B,C)\) to the straightening of \(r\) gives a functor \(\Span (\Fin )\to \Cat _{\infty }\). It sends \(I\) to \(\Fun ((\Fin _{/I})\catop ,C)\) and a span \(I\xleftarrow {f}K\xrightarrow {g}J\) to restriction along \[ (f_!g^*)\catop \colon (\Fin _{/J})\catop \longrightarrow (\Fin _{/I})\catop . \] Let \(\widetilde C^{\times }\to \Span (\Fin )\) be its cocartesian unstraightening, and let \(C^{\times }_{\mathrm {con}}\subseteq \widetilde C^{\times }\) be the fiberwise full subcategory whose fiber over \(I\) consists of the finite-product-preserving functors \((\Fin _{/I})\catop \to C\). The subscript \(\mathrm {con}\) indicates that this is the concrete model.