The Giraud-Benabou construction for splitting fibrations

Question

I'm currently reading "Revisiting the categorical interpretation of dependent type theory" and they give a very terse description of the Giraud-Benabou construction:

For a fibration $p : \mathbb E \to \mathbb B $, the fibration $Rp : R\mathbb E \to \mathbb B$ is defined by

• Obj $R\mathbb E$ is the set of pairs $(X,\phi)$ where $X \in \mathbb B$ and $\phi : \mathrm{dom}_X \to p$ is a morphism of fibrations from the restriction of the domain fibration to the slice categories $\mathrm{dom}_X: \mathbb B / X \to \mathbb B$. $Rp$ is the first projection.
• $\mathrm{Hom}((X, \phi),(Y, \psi))$ consists of pairs $(t,\mu)$ where $t : X \to Y$ and $\mu : \phi \to \psi \circ \mathrm{dom}_t$ over $\mathbb B$.

They then prove that this is a split fibration in a single line ("for $t:X \to Y$, set $\phi [t] = \phi \circ \mathrm{dom}_X$, ie. $\phi[t](s) = \phi(t \circ s)$ for all $s:Z \to X$, and $t_\phi = (t,id)$. Moreover, $Rp$ is split by the associativity of composition in $\mathbb B$"), and it isn't clear to me exactly what the relation between $Rp$ and $p$ is.

Questions:

1. Is there a slightly less terse reference for this that isn't buried somewhere in an almost 500 page book on non-abelian cohomology written in French?
2. What exactly is the relation between $Rp$ and $p$?
3. What's the intuition behind this construction? If I were trying to create a split fibration from a fibration, why might I think to do this?
4. What does this do to the codomain fibration over Set? Does this have a simple description?

Answer 1

Section 2.2 of The local universes model gives a possible answer to (2) and (3): $R$ (or $(-)_*$ in their notation) is a right adjoint to the forgetful functor from split fibrations to non-split fibrations. Their description is no less terse, but perhaps beta-reduced a bit more:

An object of $T_*$ over $\Gamma\in C$ consists of an object $A$ of $T(Γ)$, together with for each $f : \Gamma'\to \Gamma$ some cartesian lifting $\bar{f} : A_f \to A$, such that $A_{1_\Gamma} = A$, $\bar{1_\Gamma} = 1_A$.

In the case of the codomain fibration, this means that an object of $T_*$ is a morphism equipped with a chosen pullback square along every morphism into its codomain, such that the chosen pullback along the identity is the identity square.