It is well known that (working over ZF) AC implies that every [fibration](https://ncatlab.org/nlab/show/fibration) $p:\mathcal{E}\to\mathcal{B}$ can be equipped with a [cleavage](https://ncatlab.org/nlab/show/cleavage) by choosing, for each arrow $u:I\to p(X)$ in the base category whose codomain is in the image of the fibration, a Cartesian arrow $\overline u(X):u^\*(X)\to X$ in the overcategory above $u$ whose codomain is $X$.



> 
> Does the reverse implication hold?
> 
> 
> 


Andrej Bauer mentions in [this MO answer](https://mathoverflow.net/a/243187/92164) that he suspects the converse holds; I was wondering if anyone had a proof on hand.



Is AC equivalent over ZF to 'every fibration can be equipped with a cleavage'?
Yes, in fact Grothendieck fibration between groupoids are enough.


Let $p:Y \to X$ be any surjection.


We construct the following groupoid $G$. Its set of objects is $X \amalg Y$. Its morphisms corresponds to the equivalence relation such that two elements of $y$ are equivalent if they have the same image by $p$ and an element of $y$ is equivalent to its image by $p$ in $X$ (and no distinct elements of $X$ are equivalent).


We then consider $I$ the walking isomorphisms, i.e. the anti-discrete groupoid on two objects, and the functor $G \to I$ that sends element of $Y$ on one object and element of $X$ on the other.


I claim that:


1. it is a fibration. (easy to check)
2. a cleavage produces a section of $p$: for each $x \in X$ a cartesian lift of the non-identity arrow $e \to p(x)$ corresponds to the choice of a $y \in Y$ such that $p(y)=x$.


**Remark:** a more conceptual way to understand this is that a fibration over $I$ is the same as an "anaequivalence" (in the sense of Makkai anafunctors) and a cleavage for such a fibration gives choice of a pair of inverse functors implementing this equivalence. So "anyfibration admit a cleavage" implies that every anaequivalence is implemented by a pair of inverse functor, and in particular that every fully faithful essentially surjective functor has an inverse. We then combine this with the usual proof that the existence of inverse functors imply the axiom of choice.


