Constructively, are all fibrations cloven? 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.
 A: If the axiom of choice holds then every fibration is cloven, and I would not be surprised if the converse holds. So this talk about not using the axiom of choice is best understood as closet-constructivism.
Regarding extensional type theory, I would advise being very careful about doing mathematics in it. If your theory is not susceptible to a Diaconescu-style argument then I suppose you are using dependent sums $\Sigma$ instead of existentials $\exists$, and you do not have any kind of quotients or propositional truncations lying around (otherwise the ghost of Diaconescu appears). On the other hand propositional equality satisfies Uniqueness of identity proofs.
The thing to pay attention to are statements and definitions which turn from a propostion to a structure when we replace $\exists$ with $\Sigma$. Two examples:


*

*The usual definition of "$f$ is a cartesian arrow" is a statement of the form "for every ... there exist unique .... such that some equations hold". If we change this into "$\prod$ ... $\sum$ unique ... such that some equations hold" we still have an h-propostion, thanks to uniqueness and extensional equalty.

*The usual definition of "$p : E \to B$ is a fibration" is of the form "for every arrow there exists a cartesian arrow such that some equation holds". When we turn this into "$\prod$ arrow $\sum$ cartesian arrow such that equation holds" we changed "$p$ is a fibration" to "$p$ is a cloven fibration". (In fact there is no way to say "$p$ is a non-cloven fibration", is there?) Consequently, any theorem that speaks about equality of cloven fibrations changes its meaning, because we are now comparing fibrations with cleaveges.
The upshot of this is that one has to be quite careful about veryfing that everything actually works. Good luck!
A: 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.
