If I remember correctly Benabou points out that indexed categories correspond to split fibrations.
The splitting internally corresponds to a notion of equality.
The existence of a splitting for every fibration uses (is equivalent to?) the axiom of choice.
In my reading, Benabou seems to say something to the effect that in naive category theory (read ‘synthetically’) not all categories come with an equality, each such equality structure corresponds to a splitting of the fibration obtained by externalization.
If I remember correctly Benabou points out that indexed categories correspond to split fibrations. The splitting internally corresponds to a notion of equality. The existence of a splitting for every fibration uses (is equivalent to?) the axiom of choice. In my reading, Benabou seems to say something to the effect that in naive category theory (read ‘synthetically’) not all categories come with an equality, each such equality structure corresponds to a splitting of the fibration obtained by externalization.