# 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.

• If my memory serves me right, there are some constructive systems where the axiom of choice is a theorem. In those, it seems, all fibrations will be cloves of garlic. – Asaf Karagila Jun 27 '16 at 17:41
• Only if in those systems one can actually formulate enough mathematics to get to fibrations. – Andrej Bauer Jun 27 '16 at 20:22
• Certainly extensional type theory would suffice as such an example then. (Axiom of choice is a theorem there, and does not imply excluded middle, because of the functional character of universal quantification) – Jonathan Sterling Jun 27 '16 at 20:30
• The reason that AC does not imply LEM is not the functional character of universal quantification but rather lack of quotients or propositional truncation. – Andrej Bauer Jun 27 '16 at 21:01
• @AndrejBauer No, AC holds w/o LEM in ETT + quotients & propositional truncation (see Nuprl). – Jonathan Sterling Jun 27 '16 at 21:02

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.

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:

1. 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.

2. 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!

• Thanks for the answer, and especially for the remarks about what happens when you use Pi/Sigma rather than forall/exists! However, I must remark that assuming we use Pi and Sigma in ETT, we can still add quotients & truncation without falling prey to Diaconescu. Nuprl is a lovely example of this—quotients & truncation are orthogonal to choice when you formulate the hypothetical judgment properly, as is done in Nuprl. See my post for the details of why this is the case: jonmsterling.com/posts/… – Jonathan Sterling Jun 27 '16 at 21:04
• I suppose the right thing to do re: non-cloven fibrations in ETT is to use the squash type (which, as I have explained in my comments, does not cause any problems related to constructivity or LEM). Thanks again for your remarks! This is very helpful. – Jonathan Sterling Jun 27 '16 at 21:15
• I think it's pretty easy to show that if all fibrations are cloven then AC holds. Given a surjection $q:Y\to X$, let $B$ be the category with 2 objects 0,1 and $X$ the set of arrows from 0 to 1, let $E$ be the discrete category $Y$ with a new terminal object added, and let $p$ send $Y$ to 0, the terminal object to 1, and act as $q$ on arrows. Then a cleaving for $p$ supplies a section of $q$. – Mike Shulman Jun 28 '16 at 22:43
• Hmm, actually that last comment isn't quite right: the fiber of E over 0 has to be the equivalence relation on $Y$ induced by $q$, otherwise the functor isn't a fibration. But with that modification I think it works. – Mike Shulman Feb 3 at 4:26