Constructively, are all fibrations cloven?
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!
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.