Bicloven bifibrations via adjoints to reindexing functors In "Categorical Logic and Type Theory" by Bart Jacobs, in the proof of Lemma 9.1.2. Jacobs uses that $\mathbb E_u(X,Y) \cong \mathbb E_{\operatorname{Cod}(u)}(\coprod_u(X),Y)$ naturally in $X,Y$ for all $u$ if and only, if $p : \mathbb E \to \mathbb B$ is a opfibration (it was assumed that $p$ is a fibration, I don't know whether this changes something).
I tried proving the dual statement for Cartesian morphisms but all I seem to get given such natural isomorphisms are weak Cartesian lifts. I don't see why they should be stable under compositions. 
Ultimately the goal is to prove that a bicloven bifibration is equivalently given by a cleavage and left-adjoints to the induced reindexing functors. 
So what am I missing here to make this work?
 A: I think you may have spotted a gap in Jacobs' proof, as it shows only that weak (cloven) fibrations are weak bifbrations if and only if their reindexing functors have left adjoints. The reason a gap in a fibration argument may produce a weak fibration argument is that a weak fibration is a functor the restriction of which to the preimage of any subcategory of the form $\circlearrowright\to\circlearrowright$ is a fibration. Consequently, a fibration argument that does not mention composition of cartesian morphisms will only be valid for weak fibrations.
Nevertheless, it is true that being a fibration ensures $p$-weakly cocartesian morphisms are cocartesian. I'll prove the dual statement using the following relativization of the notion of cartesian.
Definition. Relative to a functor $\mathcal C\xleftarrow{p}\mathcal F$, we say that a morphism $B\xrightarrow{\gamma}C\in\mathcal F$ over $Y\xrightarrow{g}Z\in\mathcal C$ (i.e. with $p\gamma=g$) is $f$-cartesian for a morphism $X\xrightarrow{f}Y\in\mathcal C$ if every $A\xrightarrow{\eta}C$ over $X\xrightarrow{f}Y\xrightarrow{g}Z$ factors uniquely as $A\xrightarrow{\phi}B\xrightarrow{\gamma}C$ with $p\phi=f$.
A morphism in $\mathcal F$ is called weak cartesian if it is $\mathrm{id}$-cartesian, and cartesian if it is $f$-cartesian for every morphism $f$ with appropriate codomain. Dually, we say that a morphism is $f$-cocartesian if it is $f$-cartesian relative to the dual functor $\mathcal C^{op}\xleftarrow{p^{op}}\mathcal F^{op}$.
To get a feel for this relativization, consider what happens to the pullback lemma.
Lemma (Generalized Pullback lemma). Given a pair of morphism $A\xrightarrow{\phi}B\xrightarrow{\gamma}C$ over $X\xrightarrow{f}Y\xrightarrow{g}Z$ and a morphism $W\xrightarrow{h}X$, any two of the following properties imply the third:


*

*$\phi$ is $h$-cartesian

*$\gamma\circ\phi$ is $h$-cartesian

*$\gamma$ is $f\circ h$-cartesian


In particular, cartesian morphisms are closed under composition and post-cacnelation.
Proof. Assume 3., that $\gamma$ is $f\circ h$-cartesian. Then post-composition with $B\xrightarrow{\gamma}C$ gives a bijection between morphisms $D\to C$ over $W\xrightarrow{h}X\xrightarrow{g\circ f}Z$ and morphisms $D\to B$ over $W\xrightarrow{h}X\xrightarrow{f}Y$. Because post- and pre-composition commute, we obtain the equivalence of 1. and 2. 
Conversely, assume 1. and 2., and note that a morphism $D\to C$ over $W\xrightarrow{f\circ h}Y\xrightarrow{g}Z$ factors as $D\to A\xrightarrow{\gamma\circ\phi}C$, and that a morphism $D\to B$ over $W\xrightarrow{h}X\xrightarrow{f}Y$ factors uniquely as $D\to A\xrightarrow{\phi}B$.
Definition. We say that a morphism $X\xrightarrow{f}Y\in\mathcal C$ has $g$-cocartesian lifts for a morphism $Y\xrightarrow{g}Z\in\mathcal C$ if for every object $A\in\mathcal F$ over $X\in\mathcal C$ there is a $g$-cocartesian morphism $A\xrightarrow{\phi'}B'\in\mathcal F$ over $X\xrightarrow{f}Y\in\mathcal C$. We say that $\mathcal C\xleftarrow{p}\mathcal F$ is an opfibration if every morphism in $\mathcal C$ has cocartesian lifts.
Lemma. A weak cartesian $B\xrightarrow{\gamma}C$ over $Y\xrightarrow{g}Z$ is $f$-cartesian if $X\xrightarrow{f}Y$ has $g$-cocartesian lifts. In particular, weak cartesian morphisms in an opfibiration are cartesian morphisms.
Proof. If $X\xrightarrow{f}Y$ has a $g$-cocartesian lift $A\xrightarrow{\phi}B'$, then any $A\xrightarrow{\eta}C$ over $X\xrightarrow{f}Y\xrightarrow{g}Z$ factors uniquely as $A\xrightarrow{\phi}B'\xrightarrow{\gamma'}C$ with $p\gamma'=g$. Thus if $B\xrightarrow{\gamma}C$ is weak cartesian over $Y\xrightarrow{g}Z$, we have a further unique factorization $B'\xrightarrow{\beta}B\xrightarrow{\gamma}C$ over $Y\xrightarrow{\mathrm{id}_Y}Y\xrightarrow{g}Z$, hence $A\xrightarrow{\eta}C$ over $X\xrightarrow{f}Y\xrightarrow{\mathrm{id}_Y}Y\xrightarrow{g}Z$ factors uniquely as $A\xrightarrow{\phi}B'\xrightarrow{\beta}B\xrightarrow{\gamma}C$.
