The fact that any functors which is fully faithfull and essentially surjective is an equivalence of category is equivalent to the axiom of choice.

Without the axiom of choice, Makkai has introduced the notion of 'anafunctor' which generalize the notion of functors and provide inverses for the functors which are essentially surjective and fully faithful.

In a more down to earth approach:

The only thing we need to know here is when two anafunctors are isomorphic (equivalent): Let $F$ and $G$ be two anafunctors from $X$ to $Y$. One can construct a category $F \times_{X} G$ whose set of objects is $|F| \times_{|X|} |G|$ and whose morphisms are the morphism between the projection in $X$. One then has two functors from $F \times_X G$ to $Y$ given respectively by $f$ and $g$ composed with the projection to $F$ and $G$.

An isomorphism of anafunctors is given by an isomorphism between these two functors from $F \times_X G$ to $Y$.

This definition solves a lot of problems that one has when doing category theory constructively (fully faithful and essentially surjective functors becomes invertible as anafunctors, every category with binary product admit a "product anafunctor" etc...) The problem is that in general there is a proper class of anafunctors between two small categories !

Makkai proved that under some set theoretical axiom there is a set of equivalence class of anafunctors and hence that one still get a locally small category.

My question is: is it known that in ZF it cannot be proved that there is only a set of isomorphisms class of anafunctors between any two small categories, and not a proper class ?

The motivation for this question, is that the failure of this "smallness" automatically proves that a lot of classical model category structure cannot exists in ZF, and always require extra axioms (like COSHEP or the axioms Makkai introduce at the end of his paper) because localization of model category structure are always locally small. While this fact is commonly believed I've never been able to actually prove it...

Trying to construct a model category constructively is difficult. One often mention the fact that without the axiom of choice one cannot prove that the localization of the category of small categories at weak equivalence (i.e. functor which are fully faithful and essentially surjective) is locally small (ie. have small hom set) as an argument for the non existence of a model structure on cat that have these weak equivalences.

But actually proving that this cannot be proved is not easy:it can be shown that very weak choice principle like WISC or Makkai "small cardinality selection axiom" are enough to implies that this localization is locally small and we don't have that many model where those axioms fails.

My question is: Are we actually able to prove that the local smallness of this localization cannot be proved in ZF ?

I will now give some details on this, for non category theory people:

Without the axiom of choice, Makkai has introduced the notion of 'anafunctor' which generalize the notion of functors in order to describe explicitely this localization.

In a more down to earth approach, and following Makkai's paper:

The only thing we need to know here is when two anafunctors are isomorphic (equivalent): Let $F$ and $G$ be two anafunctors from $X$ to $Y$. One can construct a category $F \times_{X} G$ whose set of objects is:

$$ |F| \times_{|X|} |G| = \{ (x,y), x \in |F|, y \in |G|,, \text{ whose images in X are equal}\}$$

and whose morphisms are the morphism between the projection to $X$. One then has two functors from $F \times_X G$ to $Y$ given respectively by $f$ and $g$ composed with the projection to $F$ and $G$.

An isomorphism of anafunctors is given by an isomorphism between these two functors from $F \times_X G$ to $Y$. More explicitly:

for each $x \in |F|, y \in |G|$ having the same image in X, one has an isomorphism $\theta_{x,y}: f(x) \rightarrow g(y)$ in $Y$, such that for every $a:x \rightarrow x'$ an arrow in $F$, and $b: y \rightarrow y' $ an arrow in $G$ such that $a$ and $b$ have the same image in $X$ then one has a commutative square:

$$\theta_{x',y'} \circ f(a) = g(b) \circ \theta_{x,y}$$

Then the localization of the category of small categories at weak equivalences has the 'set' of isomorphisms class of anafunctors between $X$ and $Y$ has morphism from $X$ and $Y$, hence the claim we want to disprove is: for all small category $X$ and $Y$ there is only a set of isomorphism class of anafunctor from $X$ to $Y$.

More precisely: one wants to have a set of anafunctors such that any anafunctor is isomorphic to one in this chosen set.

Let me mention a special case that will probably be easier to understand and which I think is equivalent to the general case:

If $X$ is a discrete category (a set, seen as a category with only identity arrow) and $Y=BG$ is a category which have only one object with a group $G$ of endomorphism.

An anafunctor from $X$ to $Y$ is the data of a set $\pi:E \twoheadrightarrow X$ together with for each $a,b \in E$ such that $\pi(a)=\pi(b)$ an element $g_{a,b} \in G$ such that $g_{a,b} =g_{b,a}^{-1}$ , $g_{a,a}=1_G$ and $g_{a,b} g_{b,c} = g_{a,c}$ (indeed $g_{a,b}$ is the image of the unique morphism from $a$ to $b$ corresponding to the identity of $ \pi(a)$).

Two such anafunctors $(E,g)$ and $(E',g')$ are isomorphic if and only if there exists a function $t_{a,a'}$ which maps any pairs $(a \in E,a'\in E')$ having the same image in $X$ to $t_{a,a'} \in G$ such that $g_{a,b} t_{b,b'}= t_{a,b'}$ and $t_{a,a'} g'_{a',b'} = t_{a,b'}$.

Moreover, Makkai (still in the paper linked above) has a theory of "saturated anafunctor" which construct for each such anafunctor an isomorphic "saturated anafunctor" which in this case are anafunctors of the form:

$\pi : E \twoheadrightarrow X$ is a surjection and $E$ caries an action of $G$ such that for each $a,b \in E$ having the same image in $X$ there is a unique $g \in G$ such that $g.b= a$. One then define $g_{a,b}$ has being this unique $g$.

two such anafunctor are isomorphic if and only if they are isomorphic as set over $X$ endowed with a $G$ action.

Here again, what we want to prove more precesely is that there exists a set $F$ of anafunctors such that any anafunctor is isomorphic to one in this set.

Such anafunctor are generally called principale $G$-bundle over $X$, or $G$-torsor over $X$, and their isomorphism class form Giraud's definition of the non-abelian cohomology $H^1(X,G)$ of the discrete space $X$.

Andreas Blass has show that the triviality of all the $H^1(X,G)$ is equivalent to the axiom of choice, but here we just want to prove that they are sets.

One can formulate his definition as follow: The category of categories is a Brown category of fibrant objects, with fibrations being the isofibrations and weak equivalences being the fully faithful and essentially surjective functors (trivial fibrations are hence the functors which are fully faithful and surjective on objects).

Anafunctors $X \rightarrow Y$ are then spams $X \leftarrow Z \rightarrow Y$ where $Z \rightarrow X$ is a trivial fibrations, and we know by the work of Brown that homotopy class of such spans compute the localization of the category of categories at 'weak equivalences'.

The problem is that in general there is a proper class of anafunctors between two categories, Makkai proved that under some set theoretical axiom there is a set of equivalence class of anafunctors and hence that this localization is indeed locally small.

My question is: is it known that in only ZF it cannot be proved that this localization is locally small ? i.e. that in ZF there is not always a (small) set parameterizing all equivalences classes of anafunctors between two given categories ?

In fancy words, his definition can be formulated as follow: The category of categories is a Brown category of fibrant objects, with fibrations being the isofibrations and weak equivalences being the fully faithful and essentially surjective functors (trivial fibrations are hence the functors which are fully faithful and surjective on objects).

Anafunctors $X \rightarrow Y$ are then spans $X \leftarrow Z \rightarrow Y$ where $Z \rightarrow X$ is a trivial fibrations, and we know by the work of Brown that homotopy class of such spans compute the localization of the category of categories at 'weak equivalences'.

In a more down to earth approach:

The idea of Makkai is that an anafunctor is like a functor but where the image of an object is not uniquely defined, but, following classical categorical philosophie, only well defined up to unique isomorphism.

More precisely: If $X$ and $Y$ are (small) categories, an anafunctor from $X$ to $Y$ is the data of:

-A set $|F|$ and a surjective map $\pi: |F| \rightarrow |X|$ (where $|X|$ denotes the set of objects of $|X|$).

-On consider $F$ as a category over $X$ such that $\pi$ is extended into a fully faithful functor $\pi:F \rightarrow X$ (i.e. $Hom_F(a,b):=Hom_X(\pi(a),\pi(b))$.

-One has a functor $f$ from $F$ to $Y$.

This fits the idea explained above as follow: if you have an object $x \in X$, you compute its image by $F$ by taking any $z \in |F|$ such that $\pi(z)=x$ and taking the image of $z$ by $f$. If one chose of a different $z'$ then there is a unique isomorphism between $z$ and $z'$ which is send to the identity of $x$ and this induce a canonical isomorphism between $f(z)$ and $f(z')$.

I refer to the paper of Makkai linked above for how anafunctor are composed as it is not relevant to the question...

The only thing we need to know here is when two anafunctors are isomorphic (equivalent): Let $F$ and $G$ be two anafunctors from $X$ to $Y$. One can construct a category $F \times_{X} G$ whose set of objects is $|F| \times_{|X|} |G|$ and whose morphisms are the morphism between the projection in $X$. One then has two functors from $F \times_X G$ to $Y$ given respectively by $f$ and $g$ composed with the projection to $F$ and $G$.

An isomorphism of anafunctors is given by an isomorphism between these two functors from $F \times_X G$ to $Y$.

This definition solves a lot of problems that one has when doing category theory constructively (fully faithful and essentially surjective functors becomes invertible as anafunctors, every category with binary product admit a "product anafunctor" etc...) The problem is that in general there is a proper class of anafunctors between two small categories !

Makkai proved that under some set theoretical axiom there is a set of equivalence class of anafunctors and hence that one still get a locally small category.

My question is: is it known that in ZF it cannot be proved that there is only a set of isomorphisms class of anafunctors between any two small categories, and not a proper class ?

The motivation for this question, is that the failure of this "smallness" automatically proves that a lot of classical model category structure cannot exists in ZF, and always require extra axioms (like COSHEP or the axioms Makkai introduce at the end of his paper) because localization of model category structure are always locally small. While this fact is commonly believed I've never been able to actually prove it...