I have posted this question [here][1] 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:

> ...call two morphisms of Eq-fibrations $(K,H),(H',K') \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'$ 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.

[1]: https://math.stackexchange.com/q/2886664/11888