Theorem 23.8.3 (Currying for cartesian fibrations). Let \(p\colon E \to B\) be a cartesian fibration and let \(C\) be an \(\infty \)-category. Write \[ A := \Str ^{\ct }(p)\colon B\catop \to \Cat _{\infty }. \] Thus, for a morphism \(\beta \colon b\to b'\) in \(B\), the induced functor is the cartesian transport functor \(\beta ^*\colon E_{b'}\to E_b\). Let \[ H\colon B \to \Cat _{\infty }, \qquad b \mapsto \Fun (E_b,C), \qquad \beta \mapsto (\beta ^*)^* \] and let \(q\colon Q:=\Un ^{\cc }(H)\to B\) be its cocartesian unstraightening. Then there exists a functor \[ \ev \colon Q\times _B E \to C \] which restricts on the fiber over \(b\in B\) to the usual evaluation functor \[ \Fun (E_b,C)\times E_b \to C \] and which has the following universal property: for every object \(D\to B\) of \((\Cat _{\infty })_{/B}\), the composite \[ \Fun _{/B}(D,Q) \xrightarrow {-\times _B E} \Fun _{/B}(D\times _B E,Q\times _B E) \xrightarrow {\ev \circ -} \Fun (D\times _B E,C) \] is an equivalence of \(\infty \)-categories.
Proof. This is the dual of Gepner et al. (2017), Proposition 7.3. That result identifies the internal hom obtained by exponentiating along a cocartesian fibration as the cartesian unstraightening of the fiberwise functor categories. Passing to opposite categories gives the present statement for a cartesian fibration: the right adjoint to \(-\times _B E\) is the cocartesian unstraightening of \[ b\longmapsto \Fun (E_b,C), \] with transport given by precomposition with cartesian transport in \(E\). Its counit is the displayed evaluation functor, and the adjunction gives the asserted equivalence. □
Generated from the authoritative LaTeX source.