The 2-monad for Grothendieck fibrations Let $B$ be a category. There is a 2-monad on the slice 2-category $\mathsf{Cat}/B$, which sends $E \overset{p}{\to} B$ to the slice category $B \downarrow p$. I'm told that an algebra for this monad is a Grothendieck fibration over $B$ equipped with a splitting, whereas a pseudoalgebra is a Grothendieck fibration equippped with a cleavage. Everywhere I can find this stated in the literature, this fact is regarded as "obvious" or "an easy exercise". I'm having trouble with the exercise, even in the strict case.
An algebra for this monad will give the structure of a "transport" functor $\mathrm{trans}: B \downarrow p \to E$, $b \overset f \to p(e) \mapsto \mathrm{trans}_f(e)$. Unitality and associativity make $\mathrm{trans}$ look like a splitting of a Grothendieck fibration. The cartesian lift of $b \overset f \to p(e)$ ought to be $\mathrm{trans}_f(e)$, with the cartesian map $\mathrm{trans}_f(e) \to e = \mathrm{trans}_1(e)$ obtained by applying $\mathrm{trans}$ to the following square:
$\require{AMScd}
\begin{CD}
b @>{f}>> p(e)\\
@V{f}VV @VV{p(1)}V\\
pe @>>{1}> p(e)
\end{CD}$
regarded as a morphism in $B \downarrow p$ from the top row to the bottom row. Then we can construct lifts which should witness the universal property of this cartesian lift as follows. If $b' \overset \beta \to b$ is a morphism in $B$ and $e' \overset \varepsilon \to e$ is a morphism in $E$ such that $p(\varepsilon) = f \circ \beta$, then we apply $\mathrm{trans}$ to the square
$\require{AMScd}
\begin{CD}
pe' @>{1}>> p(e')\\
@V{\beta}VV @VV{p(\varepsilon)}V\\
b @>>{f}> p(e)
\end{CD}$
regarded as a morphism in $B \downarrow p$ from the top row to the bottom row. This produces a map $e' = \mathrm{trans}_1(e') \to \mathrm{trans}_f(e)$ lying over $\beta$. Composing the two above squares and applying functoriality and unitality of $\mathrm{trans}$ shows that we have in fact constructed a factorization as expected from the universal property of the cartesian lift constructed above.
But I don't see why this factorization is unique, as required by the universal property of a cartesian lift. Why is this so?
Probably this should follow from the general theory of colax-idempotent 2-monads, but I'm not sure how. And anyway, this would simply push back the difficulty to showing that this 2-monad is colax-idempotent.
 A: Well, I eventually figured this out, though it took me longer than I would have liked! It's a bit disorienting working with this 2-monad because you end up thinking in terms of commuting squares, and deciding when to work with the "vertical composition" of the actual categories and the "horizontal composition" of the monad must take some experience. I eventually resorted to trying to write down a minimal counterexample, and then seeing what went wrong!
Since I haven't been able to find this written down anywhere, here's one way to see that the factorizations constructed above are unique, exhibiting $\mathrm{trans}_f(e)$ as a cocartesian lift of $f$.
Notation:


*

*Write $f^\ast e$ for the object $\mathrm{trans}_f(e)$ 

*Write $f^\ast$ for the morphism $\mathrm{trans}_f(e) \to e$ (which we want to show is cartesian)


I'm not sure what a good systematic notation would be.
We want to show that if $g,g': e' \to f^\ast e$ have the property that $pg = pg'$ and $f^\ast \circ g = f^\ast \circ g'$, then $g = g'$.
Step 1: (This step is not really necessary, without it just make a few notational tweaks to the next step.) It suffices to show this in the case where $g,g'$ are vertical, i.e. $pg = pg' = 1_b$.
For we could always replace $f$ with $f \circ pg$, $f^\ast$ with $(f \circ pg)^\ast$, and $g,g'$ with their canonical factorizations $\bar g, \bar g'$ through $(f \circ pg)^\ast$. The reduction follows because $(f \circ pg)^\ast = (pg)^\ast \circ f^\ast$ and $g = (pg)^\ast \circ \bar g$, $g' = (pg)^\ast \circ \bar g'$.
Step 2: It suffices to show that 
$(\ast) \qquad \mathrm{trans}\big((1_b, f^\ast): \big(b \overset 1 \to p(f^\ast e) \big) \to \big( b \overset f \to p(e)\big)\big) = 1_{f^\ast e}$.
For we have $g = \mathrm{trans}\big((1_b,g): \big(b \overset 1 \to p(e')\big) \to \big(b \overset 1 \to p(f^\ast e)\big)\big)$, and similarly for $g'$.  If $(\ast)$ holds, then we can postcopmose with $1_{f^\ast e}$, substitute using $(\ast)$, and by functoriality of $\mathrm{trans}$, we have $g = \mathrm{trans}\big((1_b,f^\ast \circ g): \big(b \overset 1 \to p(e')\big) \to \big(b \overset 1 \to p(f^\ast e)\big)\big)$ and a similar equation for $g'$. Now the result follows since $f^\ast \circ g = f^\ast \circ g'$.
Step 3: $(\ast)$ holds.
This follows by applying the associativity property of the algebra $\mathrm{trans}$ to the diagram
$\require{AMScd}
\begin{CD}
b @>{1}>> b @>{f}>> p(e) \\
@V{1}VV @VV{f}V @VV{p(1)}V \\
b @>>{f}> pe @>{1}>> p(e)
\end{CD}$
viewed as a morphism in $B \downarrow (B \downarrow p)$ from the top row to the bottom.
A: So I was thinking about your comment, and it seems like it's actually easier to prove this lax idempotency statement than to actually do your in-depth analysis.
I worked this out in the opposite variance, so replace all of your cartesian stuff with cocartesian. This answer is really just a sketch, but it gives the gist of how to show that being an algebra for the monad is equivalent to the natural map $E\to E\downarrow B$ admitting a left adjoint fibred over B.
Recall that to prove that a  2-monad is (co?)lax-idempotent, it suffices to show that for any algebra $a:TA\to A$, the unit map $A\to TA$ is its right adjoint, and moreover, the counit of this adjunction is an equivalence.
First, we'll consider our two functors:
$$\operatorname{\tau}:E\downarrow B\to E,$$ which is the algebra structure map, and
$$\rho:E\to E\downarrow B,$$
which is the unit functor.  It is defined on objects by the formula $$e\mapsto\langle e,p(\operatorname{id}_{e})\rangle,$$ but more specifically, this functor can be expressed as the universal map into the pullback $E\downarrow B=E\times_{B} B^{\Delta^1}$ induced by the pair of maps $$E\xrightarrow{\operatorname{id}}E$$ and $$E\xrightarrow{p} B \xrightarrow{\operatorname{diag}} B^{\Delta^1}.$$
Since $E$ is assumed to be an algebra (or pseudo or whatever), unitality already tells us that we have an equivalence $\tau\rho \simeq \operatorname{id}_E$.  We'll take this equivalence to be the counit of our adjunction, so we need to extract a unit.  By looking at the diagram
$$\require{AMScd}
\begin{CD}
p(e) @>{f}>> b \\
@VV{f}V @VV{1}V \\
b @>{1}>> b
\end{CD}$$
with the constructed lift
$$e=\tau\langle e,p(\operatorname{id}_e)\rangle \to \tau \langle e,f\rangle$$ lying over the left vertical arrow (this is just an additional datum that I didn't want to typeset in a 3d diagram), we have our prospective unit, and we'll call it $\eta$ (ok, you have to check naturality and stuff, but whatever).
Moreover, since we chose our counit to just be the aforementioned equivalence, it's enough to check by 3-for-2 that the whiskerings $\tau.\eta$ and $\eta.\rho$ are equivalences.
The fact that $\eta.\rho$ is an equivalence is completely trivial using the above square, since in that case, $f=\operatorname{id}_{p(e)}$ and we're left with the interesting case of $\tau.\eta$.
But then as you observed in your Step 3, the fact that $\tau.\eta$ is an equivalence comes from functoriality and associativity with respect to that big rectangle (mine being again dual)
$$\require{AMScd}
\begin{CD}
p(e) @>{1}>> p(e) @>{f}>> b \\
@V{p(1)}VV @VV{f}V @VV{1}V \\
p(e) @>>{f}> b @>{1}>> b
\end{CD}.$$
In particular, this tells us that the whiskering $\tau.\eta$ can be obtained by applying $\tau$ to the outer rectangle, which is a identity map in $E\downarrow B$.
So I think that's a pretty nice and clean way to see it!
