Alternative construction of the Hom-functor

Remark 23.4.3. There is an asymmetry in our definition of \(\Hom _C\): we could also have considered the cartesian functor

to get a functor \(C\catop \to \LFib (C) \simeq \Fun (C,\An )\). The resulting two functors can be shown to agree with each other: more generally, for bifibrations \(E \to C \times D\) the two ways of constructing a functor \(C\catop \times D \to \An \) agree, see [Haugseng et al. (2023), Proposition 6.18].