Theorem [efr-QHXA]

Let \mathcal {D} \to \mathcal {C} be a Grothendieck fibration. For every f: X \to Y, \bar {Y} \in \mathcal {D}_Y, select a Cartesian lift f^*\bar {Y} \to \bar {Y} of f. Then there is a unique extension of f^* to a functor \mathcal {D}_Y \to \mathcal {D}_X so that the squares

commute. With this, the assignment X \mapsto \mathcal {D}_X, f \mapsto f^* assembles into a pseudofunctor \mathcal {C}^\mathrm {op} \to \mathsf {Cat}.