Lemma 1.7.2 in Bart Jacobs' "Categorical Logic and type theory", asserts that the category of all fibrations $\mathbf{Fib}$ is a fibration over $ \mathbf{Cat} $ via the codomain functor.
A morphism in $\mathbf{Fib} $ from $ q \colon \mathbb{D} \to \mathbb{A}$ to $ p \colon \mathbb{E} \to \mathbb{B}$ is a pair of functors $H \colon \mathbb{D} \to \mathbb{E}$ and $ K \colon \mathbb{A} \to \mathbb{B} $, which make the resulting square commute and $H $ must also send cartesian morphisms in $\mathbb{D}$ to cartesian morphisms in $ \mathbb{E}$.
Given a fibration $ p \colon \mathbb{E} \to \mathbb{B} $ and a functor $K \colon \mathbb{A} \to \mathbb{B}$, it was shown that the pullback of $p$ along $K$ is also a fibration. From what I understand, the resulting pullback square should give a cartesian morphism over $ K $ whose codomain is $p$, proving that $\mathbf{Fib}$ is a fibration. However, I can't seem to prove that the resulting map between the pullback and $\mathbb{E} $ preserves cartesian morphisms. It seems one has to assume some extra conditions on $K$: for example, that $K$ Is full and subjective on objects. What am I overlooking?
Thank you very much for your consideration.