I have posted this question here on M.SE but since it received little attention and since it seems difficult to find helpfule references I reposting it here.
In Jacob's Categorical logic and Type Theory in relation to fibrations with equality the author gives the following definition (Remark 3.6.6):
...call two morphisms of Eq-fibrations $(K,H),(K',H') \colon p \to q$ between two Eq-fibrations $p \colon \mathbb E \to \mathbb B$ and $q \colon \mathbb D \to \mathbb A$ equivalent if:
(1) $H=H' : \mathbb{E} \to \mathbb{D}$, and on objects $K=K' \colon \text{Obj}(\mathbb B) \to \text{Obj}(\mathbb A)$;
(2) $K(u)$ and $K'(u)$ are internally equal in $q$, for each morphism $u$ in $\mathbb B$.
This definition troubles me for the following reason.
Assume $(H,K)$ and $(H',K')$ are as above (i.e. they are an equivalent pair of morphisms of Eq-fibrations) and let $u$ be a morphism of $\mathbb B$.
Since $p$ is a fibration, and we assume that all the fibers are not empty categories (assumption reasonable for instance for the classifying fibration of an equational theory), we have a cartesian lifting of $u$, so we have a morphism $v$ in $\mathbb E$ such that $p(v)=u$.
Since by hypothesis $H=H'$ we should have $$q \circ H(v)=q \circ H'(v)$$ and since $(H,K)$ and $(H',K')$ are morphism of fibrations $$K\circ p(v) = K' \circ p(v)$$ hence $$K(u) = K'(u)\ .$$
Since we made no assumption on $u$, with the exception of being in the image of $p$ which should hold in all classifying fibration (if I am not mistaken), it seems that it should follow that $K=K'$ and so that Eq-fibration morphisms should equivalent only if they are equal, which seems counterintuitive since the author proposes it as an equivalence alternative to equality.
So here is my question.
Did I make any mistake in my argument above? In case not, how can the definition above be fixed to obtain a non trivial equivalence between Eq-fibration morphisms?
Thanks in advance for any help.
