A "cloven fibration" is a fibration for which we have an explicit choice of cartesian liftings; this is often phrased as, "We can pick a lifting without using the axiom of choice".


Firstly, I'm a bit perplexed by this language, since the intensional character of the formal proof of a statement ought not to factor in the definition / meaning of that statement. Is there a precise definition of "cloven fibration" in a classical setting which does not appeal to the intensional structure of a formal proof (namely, the use of the axiom of choice)?


I guess I am looking for an "internal" definition, which could distinguish *internally* between a (proper) fibration and a cloven fibration. The reason the usual definition makes me uncomfortable is, in a classical metatheory you cannot in fact distinguish between an object which was "constructed" using the axiom of choice and one which is effectively given, so I have trouble understanding what this definition actually means.


Secondly, suppose I am working in a constructive metatheory, such as extensional type theory (where the Axiom of Choice holds without restriction—and is not susceptible to Diaconescu's argument in this case). Then are all fibrations cloven, as far as I am concerned?


Thanks! And please let me know if there is any way in which I can improve the statement of my question.



Constructively, are all fibrations cloven?
The Elephant defines a cloven fibration as a fibration equipped with a cleavage
(B1.3), where a cleavage is a particular map lifting arrows from the base
category. This doesn't require talking about (the axiom of) Choice, though
you could also describe it as a choice of liftings. However, it is an
instance of a common "algebraicizing" move, where you remove invocations of
Choice in proofs about your objects by equipping them with particular choices
from the start. So the slogan "we can pick a lifting without using the axiom
of choice" is meant to indicate that some "algebraicization" has been done,
suggesting that we intend to write some proofs about fibrations without
invoking the axiom of choice. The proofs whose intensional character we're
referring to don't factor into the definition/meaning of cloven fibrations,
cloven fibrations factor into those proofs. I don't know about the second
question.


