Definition. The “Day hom” of fibered categories [009G]

Let \(E\) and \(F\) be two fibered categories over a semimonoidal category \({\mathopen {}\left (B,\otimes ,\alpha \right )\mathclose {}}\). We may define the “Day hom” \(E\multimap _B F\) of \(E\) and \(F\) to be the following fibered category over \(B\):

\[ E\multimap _BF :\equiv {\mathopen {}\left (\pi _1\right )\mathclose {}}_*{\mathopen {}\left ( \pi _2^*E\Rightarrow _{B\times B} \otimes ^*F \right )\mathclose {}} \]

Proof. 

First of all, we note that the pullback functor \({{\mathbf {Cat}}_{/B}}\xrightarrow {{\pi _1^*}}{{\mathbf {Cat}}_{/B\times B}}\) has a right adjoint \(\pi _1^*\dashv {\mathopen {}\left (\pi _1\right )\mathclose {}}_*\), as \({B\times B}\xrightarrow {{\pi _1}}{B}\) is (as any cartesian fibration) a Conduché functor, i.e. an exponentiable arrow in \(\mathbf {Cat}\). We have already assumed that \(E\) is a Cartesian fibration, and thus so is its restriction \(\pi _1^*E\); it therefore follows that \(\pi _1^*E\) is exponentiable. With that out of the way, we may compute the hom by adjoint calisthenics:

\[ \begin {aligned} &\mathbf {hom}_{{\mathbf {Cat}}_{/B}}{\mathopen {}\left (X\otimes _B E,F\right )\mathclose {}} \\ &\quad \equiv \mathbf {hom}_{{\mathbf {Cat}}_{/B}}{\mathopen {}\left ( \otimes _!{\mathopen {}\left ( \pi _1^*X\times _{B\times B}\pi _2^*E \right )\mathclose {}} ,F\right )\mathclose {}} \\ &\quad \simeq \mathbf {hom}_{ {\mathbf {Cat}}_{/B\times B} }{\mathopen {}\left (\pi _1^*X\times _{B\times B}\pi _2^*E,\otimes ^*F\right )\mathclose {}} \\ &\quad \simeq \mathbf {hom}_{{\mathbf {Cat}}_{/B\times B}}{\mathopen {}\left ( \pi _1^*X ,\pi _2^*E\Rightarrow \otimes ^*F\right )\mathclose {}} \\ &\quad \simeq \mathbf {hom}_{{\mathbf {Cat}}_{/B}}{\mathopen {}\left (X, {\mathopen {}\left (\pi _1\right )\mathclose {}}_*{\mathopen {}\left ( \pi _2^*E\Rightarrow \otimes ^*F \right )\mathclose {}} \right )\mathclose {}} \end {aligned} \]