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.

someconstructive systems where the axiom of choice is a theorem. In those, it seems, all fibrations will be cloves of garlic. $\endgroup$ – Asaf Karagila♦ Jun 27 '16 at 17:417more comments