Split Cartesian Fibration

A Cartesian Fibration is split if:

• $\mathrm{id}^{*}(x)=x$
• $(f\circ g)^{*}(x)=g^{*}(f^{*}(x))$

Note that this definition requires an equality on objects, so it is immediately rather suspicious. However, this is actually not so bad? Unimath has a definition here that adds some extra coherence that seems to make things work out a bit better.